#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:5 int-index]:
Ok, so if I write
{{{#!hs type family UnT (a :: Type) :: k where UnT (T (t :: k')) = t }}}
the `k ~ k'` proof for the RHS is provided by the LHS.
Roughly, yes. That instance (with kinds written explicitly) becomes `UnT k' (T k' t) = t`. So the pattern-matcher needs both kinds to be the same.
Can I write a LHS that will match on `t :: k'` for all kinds `k'` and
try to unify `k ~ k'` only on the RHS? I'm not sure what you mean here. Perhaps you're describing the type-family equivalent of the difference between {{{ instance C a a }}} and {{{ instance (a ~ b) => C a b }}} The former requires the two types to be the same, while the latter matches any types and then emits a constraint saying they're equal. If I understand your question correctly, then: no. Type families don't support that right now. Perhaps in the future. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler