[GHC] #13546: Kind error with type equality

[GHC]

#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