Improving "leftover constraints" errors

[zilinc]

No guessing in variant types. For more details see discussions below. Symptom: left-over constraints with an Exhaustive constraint. We might want to enhance it in some future.

[liamoc]

This isn't a bug?

The test case never explicitly states what variant type is wanted. The type checker will not guess it.

[liamoc]

A simpler version of the same problem is simply:

f : () -> ()
f _ =
  Success ()
  | Success obj -> ()
  | Error -> ()

[zilinc]

Hmmm. I see. If I wrote e -> (store_st, e) in the second pattern it will infer.

[liamoc]

What? e -> e? Nothing to do with it?

[liamoc]

The thing is if you write Success obj its type is unknown. It will try and work it out from context, but if you pattern match immediately on it, the only thing it knows is that it should have a Success and an Error alternative and that matching on both of them should be exhaustive.. but there are an infinite number of possible types you could give to Success obj which would satisfy those constraints. One example would be <Success Obj | Error | SomethingElse> take SomethingElse

[zilinc]

Ahh, typo. So does it really matter which one it guesses? Any minimal type that doesn't introduce inconsistency should be ok for this purpose?

[liamoc]

Guessing will introduce really strange results. Remember that <Success Obj> is now not a subtype of <Success Obj | Error>. Guessing a minimal type will give annoying errors like that, unless you do some sort of global guessing based on the entire constraint graph.

[zilinc]

Quite annoying --- is there a way to generate a meaningful error message for that?

[liamoc]

Well, if there is a leftover constraint like Exhaustive ?x [....] then that means you're pattern matching on an unknown type and that's going to need a signature somewhere. So we could emit special errors for that case.

Alternatively I could try do to some sort of guesswork -- it would work out okay if you take the entire constraint system into account. But it really feels like it should at least generate a warning if it's doing that. For example, if you have a bunch of code:

 let r =  .... blah blah...
      | some case -> First ()
      | some other case -> First ()
 in r
  | First x -> ....
  | _ -> ....

Then the minimal "guess" would be that the type is just <First ()>, but this would mean that the entire second branch is just dead code -- almost certainly a mistake..

[liamoc]

Did this error actually come up in Bilby? Is it easy to add a type signature to it?

[zilinc]

In that case you mentioned, it makes sense to emit an error -- if you don't say what the type is, you cannot do _ in patter matching.

[zilinc]

It's extracted from bilby. It's possible to add some annotation but in general, the patterns could be large (consequently the types) and with several levels of pattern matching, it requires quite a bit of thinking to understand where guidance is required. Pattern matching is a big feature in FP and it would resist user to write idiomatic functional-style code in Cogent.

[liamoc]

Thinking about it more, I don't think we can safely guess.

If we have a constraint Exhaustive ?x [Success a, Error] then if we're guessing we'll just transform that to ?x :< <Success ?y | Error>. Seems fine, right?

The problem is that we only want to guess if there isn't an obvious solution for ?x that doesn't require guessing. Otherwise the "guessed" solution would override the "real" solution. But, if we delay introducing the guess constraint, then that delay could mean that other variables are solved without benefit of information learned from the guess constraint and we'd end up with issue #22 style bugs all over again, but only in rare, hard-to-debug cases.

One little trick to make things easier is to make a constructor function that specifies the type, e.g:

success : all (a,b). a -> R a b
success a = Success a

Then use success instead of Success and your errors should be gone ;)

[zilinc]

Looks like a fare trick. After applying that trick, I still got lots of leftovers, which does NOT consist of loops or exhaustive constraints. I need to study more on the original code in order to tell what's going on.
All the leftover constraints are as below: (* indicate reflexive >: relation)

144 >: 2344* >: 2342 >: 2340 >: 2338 >: 58*
                  |       |
                  |       +--------- >: 103*
                  +------ >: 124* 

SomeConcreteType :> 144!           Share 144!

[liamoc]

It looks like this might be another situation where they misused !. Note that if ?144 wasn't banged it'd work just fine.

Also, that's a lot of unification variables...

[zilinc]

Not sure that's the case, as pass_ticket_e31.cognet also suffers from the same problem.