Inferencer fails to figure out ! on typevars

[zilinc]

Synopsis

The Problem

In a nutshell, if there's a function whose type includes a forall quantified type variable a (for example) and a! appears in the type signature, then it's very likely you'll encounter a constraint of the form (?0)! :< T which is unsolvable by the constraint solver and you'll get a typecheck error of leftover constraints.

The Solution

If possible, avoid this form of type signature. Instead, use explicit constraints, like forall (a :< DS). .... There're cases where it is impossible to do so. In that case, you have to explicitly do the type application like f [U8, Bool, A] yourself. Note that partial type application is allowed, and holes are supported so you can only apply the type that is in question. E.g. f [_, Bool].

Also see discussion in #22 and 255f000

[liamoc]

So, it's worth noting that given a constraint:

(?x)! :< T

we can't solve ?x directly because it's impossible to undo ! (it's not injective). It won't be possible to fix this easily. In that test, it knows you passed in an obsv! of type (), but there's no way for it to (in general) figure out what obsv is just from what obsv! is. There are some special cases (like ()) where it works, but I don't think we want to go down that route.

One thing we might want to do is to emit a better error message for this scenario than "leftover constraint". We might want to examine what the leftover constraint is and give a more helpful error message in some other scenarios too.

But I'm pretty much taking the position that this isn't a bug, but rather just an incompleteness of the inference algorithm that can be worked around.

[zilinc]

Agreed. That's why I didn't tag it a bug. Some heuristics can be used to solve some obvious cases, but I'd leave it as future work.

[zilinc]

Better error messages (and in general) is much appreciated, otherwise it will force me to be around when someone is using the language :P

[zilinc]

Alternatively an easier workaround would be to have some type holes syntax, so that users can help the compiler know the instantiation of the outstanding typevars, without having to annotate all type args.

[liamoc]

That would be nice to have. Right now you can partially apply type args, but you can't apply later args without applying earlier args first.

I think a better workaround is to use the kind system though. That's what it's there for.

[zilinc]

What about things like wordarray_get: all(a :< DSE). ((WordArray a)!, WordArrayIndex) -> a? Is there a way to utilise kind system? This one gives leftover constraints, expectedly.

[liamoc]

That ! should be harmless?

[zilinc]

I got

Leftover constraint!
U8 :< (?1)!

Leftover constraint!
(?1)! :< (?1)!

Leftover constraint!
Escape ?1

Leftover constraint!
Drop ?1

Leftover constraint!
Share ?1

[zilinc]

With/out the [a]s I get different errors.

[liamoc]

This is another one of those situations where we could solve that ! constraint...

I'm thinking that we should solve them whenever we can...

I just need to isolate the cases where it's possible clearly.

[liamoc]

I guess it's always possible to un-! a type if no ReadOnly or Writable sigils occur in it..

[zilinc]

If it's w, then _|_; r needs some guessing, I think.

[zilinc]

With what we have now, typeargs are not in a situation that's much better than what we had before. Selectively removing/adding them is brain intensive. Doing a bit more keystrokes saves brains.

[liamoc]

Hm, so the only problem with our guessing strategy is that we can't tell whether any r sigils exist without fully expanding all type synonyms, and currently (for error message reasons) the solver only simplifies to WHNF.

[zilinc]

Do we have to know what ?0 is for well-typedness? Can we solve up to (?0)! (i.e. make it an atomic unif. var-ish thing) and substitute (?0)!, and in a later stage try to guess ?0?

[liamoc]

That would just end up with the same constraints but for the new unif. var.

One option would be to solve them up to WHNF, e.g if you have:

 (?1)! :< (T,U) 

then we generate fresh ?2 and ?3 and produce:

 (?2)! :< T
 (?3)! :< U

But I'd have to add rules for every single type modulo !... I'm trying to figure out a way to make that easier..

[zilinc]

Some real examples: in rbt.cogent, there're things like:

rbt_next: all (k :< DS, v :< DS). ((Rbt k v)!, k!) -> R k ()

type RbtConsumeF k v acc obsv = RbtElemAO k v acc obsv -> acc
type RbtCondF k v acc obsv = (RbtElemAO k v acc obsv)! -> Bool

rbtFTrue: all(k:< DS, v :<DS, acc, obsv). RbtCondF k v acc obsv
rbtFTrue _ = True

[vjackson725]

This should be somewhat mitigated by Amos and my changes to type inference in Sink/Float. The only place this should occur now is when you have variables under bangs on both sides of the constraint.