Re: [GHC] #12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?)

[GHC]

#12102: “Constraints in kinds” illegal family application in instance (+
documentation issues?)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13780            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I was just about to do this. But then I had second thoughts. Right now, we
 take it as a general rule that the following two declarations are the
 same:

 {{{#!hs
 data G1 a where
   MkG1 :: G1 Bool

 data G2 a = (a ~ Bool) => MkG2
 }}}

 and indeed this is true today. But if we throw out `~` in kinds, as
 proposed here, then only `'MkG1` would be usable in a type. `'MkG2` would
 be an error, violating our general rule.

 About Givens: GADT pattern-matching in terms must be very fancy, because
 the GADT pattern-match relates a runtime thing to a compile-time thing.
 Figuring out how to do this time travel required several PhDs to be
 earned. On the other hand, GADT pattern-matching in types need not be
 nearly so advanced, because everything is compile-time. Indeed, GHC's
 current implementation of type-level GADT pattern-matching is somewhat
 simplistic, not using Givens at all. (More below, as I'm sure you'll be
 curious.) So, even though a `~` in a kind never gives rise to a Given,
 they are still useful and can be matched against in a type family.

 How type-level GADT pattern matching works: Let's look at an example.

 {{{#!hs
 type family F1 (a :: G k) :: k where
   F1 MkG1 = True
 }}}

 This would seem to require fancy GADT pattern matching. After all, we
 declare that the return kind be `k` for some unknown `k`, and yet we
 return `True :: Bool`. However, this really works by doing ''kind-
 matching''. That is, the definition is elaborated to make its kind
 variables explicit:

 {{{#!hs
 type family F1 (k :: Type) (a :: G k) :: k where
   F1 Bool MkG1 = True
 }}}

 Because type families can pattern-match on kinds, this is hunky dory. The
 ''caller'' is responsible for showing that `k` is really `Bool`. This
 sounds terrible, though: what has happened to the expressiveness of GADTs?
 Nothing bad. Of course the caller can figure out what `k` should be,
 because it has the same information this function does. (This is very
 different in terms, where a GADT parameter is learned by a ''runtime''
 pattern match. No phase distinction in type families!)

 This trick has its limits, of course: you can't usefully use a constraint
 of the form `F a ~ G a` in a kind. I do want to fix that some day. But not
 today. And, in the meantime, it's unclear if I should fix this ticket and
 violate the general rule at the top of this comment.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12102#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler