#9725: Constraint deduction failure -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard, why do you think this is a bug? Looking at the simplified reproduction test case, we see {{{ -- Restricted kind signature: --test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) test :: forall ent. (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) }}} The program typechecks fine with "restricted kind signature" (agreed?), with GHC 7.8.2 or HEAD. So decomposition of type applications is working fine (i.e. comment:1 is not right; although in previous versions of GHC Reid was correct). The actual problem is that the type signature (the one not in comments) kind-checks like this: {{{ test :: forall k. forall (ent :: k -> En). (forall (i::k). Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) }}} The pattern-match on `Mb` indeed yields the given equality `ent::k ~ M::Bool`. But we can't ''use'' that unless we know that `k~Bool` and, until Richard implements kind-level equalities, we don't know that. The "restricted kind signature" de-polymorphises" it, which is all you need to make it work. Richard: you should add this to your test suite for kind-level equalities! Is there a wiki page for this? Is it [wiki:DependentHaskell]? I suspect not. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler