#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