#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 heisenbug): Replying to [comment:6 simonpj]: ... snip ...
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.
But isn't this just plain ''kind inference'' as we have it today?
The "restricted kind signature" de-polymorphises" it, which is all you
need to make it work. Right, that's what I figured. But in my ''actual'' code I have {{{ data En = M Bool | Ind Nat -- etc. data Fac :: En -> * where Mo :: Kn (M b) => Fac (M b) Odu :: Kn (Ind n) => Fac (Ind n) -- etc. }}} And the pattern match in `h` goes over these, so I *need* the poly- kindedness. It would let me consolidate a bunch of otherwise identical functions (modulo constructor names).
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:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler