unhelpful error message while unifying identical types

[rgrover]

I get a cryptic error message while lifting a Preorder relationship to Maybe. The type-checker is unable to unify identical types.

Steps to Reproduce

Using the definition of Preorder from Idris1:

interface Preorder a (rel : a -> a -> Type) where
  transitive : (x : a) -> (y : a) -> (z : a) -> rel x y -> rel y z -> rel x z
  reflexive : (x : a) -> rel x x

-- Proof of Preorder relationship over Maybe values.
export
data MaybePreorder : Maybe a -> Maybe a -> Type where
  AnythingIsBetter : MaybePreorder Nothing x
  Lift : Preorder a rel => rel x y -> MaybePreorder (Just x) (Just y)

-- If `a` has a Preorder relationship `rel`, then `Maybe a` has a lifted
-- Preorder relationship.
Preorder a rel => Preorder (Maybe a) MaybePreorder where
  reflexive Nothing = AnythingIsBetter
  reflexive (Just x) = Lift $ reflexive {rel=rel} x

  transitive Nothing y z xy yz = AnythingIsBetter
  transitive (Just x) (Just y) (Just z) (Lift v) (Lift w) =
    Lift $ transitive x y z v w

Expected Behavior

The code above should type check.

Observed Behavior

Test.idr:21:39--21:41:While processing right hand side of transitive at Test.idr:20:3--148:1:
Can't solve constraint between:
	rel x y
and
	rel x y

If I remove {rel=rel} from the definition of transitive:

  transitive (Just x) (Just y) (Just z) (Lift v) (Lift w) =
    Lift $ transitive x y z v w

I get a variant:

Test.idr:21:31--148:1:While processing right hand side of transitive at Test.idr:20:3--148:1:
Can't solve constraint between:
	rel y z
and
	rel y z
Error(s) building file Test.idr

I also get a different error message when I leave out {rel=rel} from the defintion of reflexive, but let's leave that for now.

[gallais]

This is #35

In the meantime, if you're wondering how to get out of this predicament: parametrise MaybePreorder over rel. At the moment there is no connection whatsoever between the (implicitly-bound) rel used in Lift and the one brought into scope by the Preorder a rel => constraint.

[rgrover]

@gallais:

In the meantime, if you're wondering how to get out of this predicament: parametrise MaybePreorder over rel.

Thanks for the suggestion. I'm still not out of this predicament. I've now indexed MaybePreorder with rel (and simplified Preorder to only require reflexive):

interface Preorder a (rel : a -> a -> Type) where
  reflexive : (x : a) -> rel x x

-- Proof of Preorder relationship over Maybe values.
export
data MaybePreorder : (a -> a -> Type) -> Maybe a -> Maybe a -> Type where
  AnythingIsBetter : MaybePreorder rel Nothing x
  Lift : {rel : a -> a -> Type} -> rel x y -> MaybePreorder rel (Just x) (Just y)

-- If `a` has a Preorder relationship `rel`, then `Maybe a` has a lifted
-- (MaybePreorder rel) relationship.
Preorder a rel => Preorder (Maybe a) (MaybePreorder rel) where
  reflexive Nothing = AnythingIsBetter {x=Nothing}
  reflexive (Just x) = Lift {rel} $ reflexive {rel} x

and Idris2 complains with the error rel is not accessible in this context:

MaybePreorder.idr:14:29--14:34:While processing right hand side of reflexive at MaybePreorder.idr:14:3--19:1:
rel is not accessible in this context at:
14	  reflexive (Just x) = Lift {rel} $ reflexive {rel} x
	                            ^^^^^

How do I convince Idris to use the rel it has from the instance of Preorder a rel?

[gallais]

The message comes from the fact you have introduced rel with an unlimited quantity in the definition of Lift but you don't have access to it in the body of the interface implementation.

This should be enough:

  Lift             : rel x y -> MaybePreorder rel (Just x) (Just y)

And then this should work:

  reflexive Nothing = AnythingIsBetter
  reflexive (Just x) = Lift (reflexive x)

However for a reason I do not understand this last line leads to a unification error.

1/1: Building Preorder (Preorder.idr)
Preorder.idr:16:24--17:1:While processing right hand side of reflexive at Preorder.idr:16:3--17:1:
Can't solve constraint between:
	?argTy [no locals in scope]
and
	a
Error(s) building file Preorder.idr

Looks like a bug to me.

[gallais]

You can make the error go away by changing the type of Lift to:

  Lift             : {0 x, y : a} -> rel x y -> MaybePreorder rel (Just x) (Just y)

or

  Lift             : rel x y -> MaybePreorder {a} rel (Just x) (Just y)

It seems to be the case that Idris does not generalise over a in Lift unless it appears somewhere in the telescope. I guess the generalisation pass needs to be followed up by a secondary one post unification to close the telescope of the various data constructors. Thoughts @edwinb?

[rgrover]

Thanks so much for investigating this. Your suggestions work, but I find it difficult to reason about them. Hopefully, Idris will do the right thing without requiring a workaround.

[gallais]

With :set showmachinenames you now get:

Error: While processing right hand side of transitive. Can't solve constraint
between: {rel:1167} y z and {rel:1165} y z.

So it should at least be a bit easier to diagnose the issue.

[gallais]

It seems to be the case that Idris does not generalise over a in Lift unless it appears somewhere in the telescope. I guess the generalisation pass needs to be followed up by a secondary one post unification to close the telescope of the various data constructors.

That's what the type of Lift seems to suggest:

{0 y : ?argTy} -> {0 x : ?argTy} -> {0 rel : ?argTy -> ?argTy -> Type} ->
rel x y -> MaybePreorder {a = ?argTy} rel (Just {ty = ?argTy} x) (Just {ty = ?argTy} y)

Are we somehow using a ? instead of an _ here?