[GHC] #7786: strange errors when deducing constraints

[GHC]

#7786: strange errors when deducing constraints
-----------------------------+----------------------------------------------
Reporter:  heisenbug         |          Owner:                  
    Type:  bug               |         Status:  new             
Priority:  normal            |      Component:  Compiler        
 Version:  7.7               |       Keywords:                  
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
 Failure:  None/Unknown      |      Blockedby:                  
Blocking:                    |        Related:                  
-----------------------------+----------------------------------------------
 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!

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7786>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler