#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:8 simonpj]:
No it's not just kind inference. Do you want that poly-kinded type for `test`? Sounds as if the answer is "yes". Well, then `k` is a skolem variable, and if it is is locally known to be equal to `Bool`, that's a local kind equality (a la GADTs).
While I suspected that this could be the answer, I am still happy I asked! Thanks for explaining.
From what you say, in some branches of `h`, you have a local equality `k ~ Bool` and in others you have `k ~ Nat`.
Exactly. `k` will be instantiated to different kinds in the pattern matching process.
This is just what Richard is working on!
Good to hear. Is there an ETA for this work? Is there a chance to have a stripped-down version of that feature as a preview, that handles just such plain equations, without the full bells&whistles goodness? Would a plain mortal like me be in a position to make the former happen?
Simon
Thanks again, Gabor -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler