Support fixpoint-fixing under recursion variables

Sometimes, we might need to fixpoint-fix a unification like

[ Bar [ Bar <a>, Foo ], Foo ] as <a>  🛠️  [ Bar <b>, Foo ] as <b>

where we hit a comparison between <a> and <b>. In this case, follow each
recursion point independently and see if we can find the chain to the needle
we were searching for.

Closes #5476
This commit is contained in:
Ayaz Hafiz 2023-06-13 17:14:14 -05:00
parent b3c598fcf6
commit 49a92e5ef1
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 65 additions and 1 deletions

View file

@ -92,6 +92,9 @@ flags! {
/// Prints all type mismatches hit during type unification.
ROC_PRINT_MISMATCHES
/// Prints all type variables entered for fixpoint-fixing.
ROC_PRINT_FIXPOINT_FIXING
/// Verifies that after let-generalization of a def, any rigid variables in the type annotation
/// of the def are indeed generalized.
///

View file

@ -0,0 +1,19 @@
interface Test exposes [main] imports []
Term : [
Bar Term,
Foo,
]
f = \list ->
when list is
# ^^^^ List ([Bar [Bar a]*, Foo]* as a)
[] -> Foo
[b] -> b
[b, ..] -> Bar (Bar b)
whatever : Term -> Str
whatever = \_ -> "done"
main = whatever (f [])
# ^^ List ([Bar a, Foo] as a)

View file

@ -1,5 +1,8 @@
//! Fix fixpoints of recursive types.
use roc_debug_flags::dbg_do;
#[cfg(debug_assertions)]
use roc_debug_flags::ROC_PRINT_FIXPOINT_FIXING;
use roc_error_macros::internal_error;
use roc_types::subs::{Content, FlatType, GetSubsSlice, Subs, Variable};
@ -80,6 +83,19 @@ struct Update {
/// to decide it.
#[must_use]
pub fn fix_fixpoint(subs: &mut Subs, left: Variable, right: Variable) -> Vec<Variable> {
dbg_do!(ROC_PRINT_FIXPOINT_FIXING, {
eprintln!("🛠️🛠️🛠️🛠️🛠️🛠️🛠️🛠️ BEGIN FIXPOINT FIXING 🛠️🛠️🛠️🛠️🛠️🛠️🛠️🛠️");
eprintln!(
"🛠️🛠️ ({:?}-{:?}): {:?} {:?} 🛠️ {:?} {:?}",
subs.get_root_key_without_compacting(left),
subs.get_root_key_without_compacting(right),
left,
subs.dbg(left),
right,
subs.dbg(right),
);
});
let updates = find_chain(subs, left, right);
let mut new = vec![];
@ -93,6 +109,10 @@ pub fn fix_fixpoint(subs: &mut Subs, left: Variable, right: Variable) -> Vec<Var
new.push(source_of_truth);
}
dbg_do!(ROC_PRINT_FIXPOINT_FIXING, {
eprintln!("🛠️🛠️🛠️🛠️🛠️🛠️🛠️🛠️ END FIXPOINT FIXING 🛠️🛠️🛠️🛠️🛠️🛠️🛠️🛠️");
});
new
}
@ -164,6 +184,16 @@ fn find_chain(subs: &Subs, left: Variable, right: Variable) -> impl Iterator<Ite
let left = subs.get_root_key_without_compacting(left);
let right = subs.get_root_key_without_compacting(right);
dbg_do!(ROC_PRINT_FIXPOINT_FIXING, {
eprintln!(
"❓ ({:?}-{:?}): {:?} 🔗 {:?}",
left,
right,
subs.dbg(left),
subs.dbg(right),
);
});
if (left, right) == needle {
return Ok(vec![needle]);
}
@ -180,7 +210,19 @@ fn find_chain(subs: &Subs, left: Variable, right: Variable) -> impl Iterator<Ite
| (FlexAbleVar(..), FlexAbleVar(..))
| (Error, Error)
| (RangedNumber(..), RangedNumber(..)) => Err(()),
(RecursionVar { .. }, RecursionVar { .. }) => internal_error!("not expected"),
(RecursionVar { structure: left_rec, .. }, RecursionVar { structure: right_rec, .. }) => {
// This might be a case like fix-point fixing
//
// [ Bar [ Bar <a>, Foo ], Foo ] as <a> 🛠️ [ Bar <b>, Foo ] as <b>
//
// where we hit a comparison between <a> and <b>. In this case, follow each
// recursion point independently and see if we can find the chain to the needle
// we were searching for.
let search_deeper_left = |_| help(subs, needle, *left_rec, right);
let search_deeper_right = |_| help(subs, needle, left, *right_rec);
let chain = search_deeper_left(()).or_else(search_deeper_right)?;
Ok(chain)
}
(RecursionVar { structure, .. }, _) => {
// By construction, the recursion variables will be adjusted to be equal after
// the transformation, so we can immediately look at the inner variable. We only