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.

[zilinc]

Solution: apply typeargs manually. Improvements:

• [x] type holes
• [x] type annotations on expressions
• [ ] error messages

[zilinc]

One thing weird is that is requires me to supply type arguments of error function in all invocations in all branches, which I thought one should be enough.

[liamoc]

That makes sense to me. error is a polymorphic function. You could bind the monomorphic function if you want to use the same type everywhere.

let myerror = error[...]

[zilinc]

Btw, most (>90%) of the unif vars are introduced in the solver.

[liamoc]

That makes sense. Are you noticing severe performance problems? If they exist, I can take some shortcuts when solving that should cut down on unif. vars.

[zilinc]

For the file I just committed, if I leave out the typearg on the line with a comment, it fails to infer; but for some other branches, good to do so. I (the users) cannot summaries where it's required and where not. Shouldn't all branches just unify to be the same type?

[zilinc]

performance is ok. 9s to typecheck BilbyFs (the old one 4.5s). just quite difficult to track them.

[liamoc]

I just pushed to my branch a commit that will (slightly) improve Leftover Constraint error messages. The issue #29 ticket now gives the following errors:

A subtyping constraint U8 :< (?1)! can't be solved because the RHS is unknown and uses non-injective operators (like !).
-- The unknown ?1 originates from the term at location "././tests/pass_ticket-e29.cogent" (line 12, column 18)
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 35))
      buf.data
   has type
      (WordArray (?1)!)!
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length buf.data
   has type
      U32
   in the 1st alternative buf
   in the definition at ("././tests/pass_ticket-e29.cogent" (line 11, column 1))
   for the function buf_length
A subtyping constraint (?1)! :< (?1)! can't be solved because both sides are unknown.
-- The unknown ?1 originates from the term at location "././tests/pass_ticket-e29.cogent" (line 12, column 18)
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length
   has type
      (WordArray (?1)!)! -> U32
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length buf.data
   has type
      U32
   in the 1st alternative buf
   in the definition at ("././tests/pass_ticket-e29.cogent" (line 11, column 1))
   for the function buf_length
Constraint Escape ?1 can't be solved as it constrains an unknown.
-- The unknown ?1 originates from the term at location "././tests/pass_ticket-e29.cogent" (line 12, column 18)
The constraint was emitted as it is required by the type of wordarray_length (type variable a )
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length
   has type
      (WordArray (?1)!)! -> U32
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length buf.data
   has type
      U32
   in the 1st alternative buf
   in the definition at ("././tests/pass_ticket-e29.cogent" (line 11, column 1))
   for the function buf_length
Constraint Drop ?1 can't be solved as it constrains an unknown.
-- The unknown ?1 originates from the term at location "././tests/pass_ticket-e29.cogent" (line 12, column 18)
The constraint was emitted as it is required by the type of wordarray_length (type variable a )
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length
   has type
      (WordArray (?1)!)! -> U32
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length buf.data
   has type
      U32
   in the 1st alternative buf
   in the definition at ("././tests/pass_ticket-e29.cogent" (line 11, column 1))
   for the function buf_length
Constraint Share ?1 can't be solved as it constrains an unknown.
-- The unknown ?1 originates from the term at location "././tests/pass_ticket-e29.cogent" (line 12, column 18)
The constraint was emitted as it is required by the type of wordarray_length (type variable a )
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length
   has type
      (WordArray (?1)!)! -> U32
   when checking that the expression at ("././tests/pass_ticket-e29.cogent" (line 12, column 18))
      wordarray_length buf.data
   has type
      U32
   in the 1st alternative buf
   in the definition at ("././tests/pass_ticket-e29.cogent" (line 11, column 1))
   for the function buf_length
Compilation failed!

[liamoc]

While this is very verbose, at least you can tell that a unknown introduced by the wordarray_length call can't be deduced.

[zilinc]

Even better, for things that we know, we can suggest possible fixes.