strange errors when deducing constraints

Please load attached file in ghci and observe the resulting error message. I have added my commentaries inline to what appears fishy to me. All may technically be ok, but look quite confusing.

[1 of 1] Compiling Main             ( pr7786.hs, interpreted )

pr7786.hs:74:22:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with 'Empty [KeySegment]
    Inaccessible code in
      a pattern with constructor
        Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
      in a pattern binding in
           'do' block

Yes, ok, (Nil :: Sing Empty) does not unify with (forall xxx. Nil :: Sing xxx).

    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the pattern: Nil
    In the pattern: Nil :: Sing xxx
    In a stmt of a 'do' block:
      Nil :: Sing xxx <- return
                           (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)

pr7786.hs:78:31:
    Could not deduce (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv
                      ~ 'Empty [KeySegment])
    from the context (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv
                      ~ 'Empty [KeySegment])

This one is highly disturbing. I think the user should never see such a message. Scary. This is the reason for the ticket.

      bound by a pattern with constructor
                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
               in a pattern binding in
                    'do' block
      at pr7786.hs:74:22-24
    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the second argument of `($)', namely `Sub db k sub'
    In a stmt of a 'do' block: return $ Sub db k sub
    In the expression:
      do { Nil :: Sing xxx <- return
                                (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 74 and uncomment l. 75 and reload:

pr7786.hs:75:22:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with `Intersect
                          [KeySegment] (BuriedUnder sub1 k1 ('Empty [KeySegment])) inv1'

Hmm, I vaguely understand why those new degrees of freedom arise.

    NB: `Intersect' is a type function, and may not be injective

Probably irrelevant, no need to backwards guess here, as we have -XScopedTypeVariables turned on.

    The type variables `sub', `k', `inv' are ambiguous
    Expected type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub1 k1 ('Empty [KeySegment])) inv1)
      Actual type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv)
    Relevant bindings include
      addSub :: Database inv1
                -> Sing [KeySegment] k1
                -> Database sub1
                -> Maybe (Database (BuriedUnder sub1 k1 inv1))
        (bound at pr7786.hs:74:1)
      db :: Database inv1 (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k1 (bound at pr7786.hs:74:11)
      sub :: Database sub1 (bound at pr7786.hs:74:13)
    In the pattern:
      Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv)
    In a stmt of a 'do' block:
      Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return
                                                                     (buryUnder (dbKeys sub) k Nil
                                                                      `intersectPaths` dbKeys db)
    In the expression:
      do { Nil :: Sing ((sub `BuriedUnder` k) Empty
                        `Intersect` inv) <- return
                                              (buryUnder (dbKeys sub) k Nil
                                               `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 75 and uncomment l. 76 and reload:

[1 of 1] Compiling Main             ( pr7786.hs, interpreted )


pr7786.hs:76:51:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with 'Empty [KeySegment]
    Expected type: Sing (Inventory [KeySegment]) ('Empty [KeySegment])
      Actual type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv)

Err... But (Nil :: Sing Empty) is exactly the annotation on the Nil constructor in the GADT definition!

    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the first argument of `return', namely
      `(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)'
    In a stmt of a 'do' block:
      Nil :: Sing Empty <- return
                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
    In the expression:
      do { Nil :: Sing Empty <- return
                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 76 and uncomment l. 77 and reload:

All is dandy!

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture