Unification tries to unify irrelevant things and fails to do so

[buzden]

Steps to Reproduce

This is a shrunk from a real code, so it lacks practicality, but still reveals strange behaviour. Consider the following definitions:

data E = MkE Unit

data P : E -> Type where

data X : E -> Type

empty : X $ MkE ()

mk : P a => X a -> X b

foofu : Nat -> X a
foofu n = mk $
  case n of
    Z => empty
    _ => ?foo_1

Expected Behavior

While processing right hand side of foofu. Can't find an implementation for P ?a.

Observed Behavior

Error: While processing right hand side of foofu. When unifying:
    X (MkE ())
and:
    X ?a
Mismatch between: Nat and ().

UnifBug:14:10--14:15
 10 | 
 11 | foofu : Nat -> X a
 12 | foofu n = mk $
 13 |   case n of
 14 |     Z => empty
               ^^^^^

---

Everything seems to be important. This particular bug goes it you do not match particular cases in case, or even if you remove where from definition of P, or if you remove the Unit parameter from MkE.

---

This error is strange in both parts.

At first, X (MkE ()) and ?a really should unify. Second, why Idris tries to unify types Nat and ()? There is nothing here about it.

Moreover, we've realised that this function always tries to unify the type of the first parameter of foofu and the type of argument of MkE. I.e., if you change definitions to

data E = MkE (Maybe Unit)

data P : E -> Type where

data X : E -> Type

empty : X $ MkE $ Just ()

mk : P a => X a -> X b

foofu : String -> X a
foofu n = mk $
  case n of
    "" => empty
    _  => ?foo_1

you get

Mismatch between: String and Maybe ().

[dunhamsteve]

A couple notes from my investigation into the issue:

I dropped the P a => to get a different test case. It gives a slightly different unification error. In the String case, without the P a =>, I see this in the logs:

LOG unify.hole:10: Unifying: Main.{a:847} [a[1], ""] with ($resolved2555 ($resolved927 $resolved2532 $resolved2536))
LOG unify.postpone:10: Not in pattern fragment: (Main.MkE (Prelude.Types.Just Builtin.Unit Builtin.MkUnit)) =?= ?Main.{a:847}_[a[1], ""]

It appears to have a NPrimVal _ (Str "") in args which causes getVars and then patternEnv to fail. With the P a => in place, the meta is marked as invertible and it calls unifyHoleApp which then tries to unify the first arguments, causing that weird comparison of () and String.

I later see the following log messages, which suggest to me that the "" was n[0]@"" at the term level:

LOG unify:20: Comparing type constructors Main.X and Main.X
LOG unify:20: Constructor $resolved2566
LOG unify:20: Term: : (Main.MkE (Prelude.Types.Just Builtin.Unit Builtin.MkUnit))
LOG unify:20:   : (Main.MkE (Prelude.Types.Just Builtin.Unit Builtin.MkUnit))
LOG unify:20: 
LOG unify:20: Term: : ?Main.{a:847}_[a[1], n[0]@""]
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:847}
LOG unify:20:   : ?Main.{a:847}_[a[1], ""]
LOG unify:20: 

I'm not sure how to prevent the n from turning into a string.