#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