#14331: Overzealous free-floating kind check causes deriving clause to be rejected -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T14331 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've clarified point 3, above. Replying to [comment:32 RyanGlScott]:
5. c. I'm not sure I understand this business about `kappa2` (or why
you'd choose `kappa2 := Type`). Can you give an example of where this would arise? {{{#!hs class C a data D a = D deriving C }}} We see that `C :: forall k. k -> Constraint`. So we have `ki` = `forall k. k -> Constraint`. We then instantiate (note new step, above) to get `ki` = `kappa3 -> Constraint`, where `kappa3` is a fresh unification variable. Unifying with `kappa -> Constraint` simply sets `kappa := kappa3`. So, `ki2` is really just `kappa3`. This is the special case in (d). What's really going on here is that both the following are well-kinded: {{{#!hs instance C D instance C (D a) }}} We choose the second -- that's the `kappa2 := Type`. Alternatively, we could issue an error here; it's all a free design choice.
5. e. Some more validity checks that would need to be performed for data
family instances are documented [http://git.haskell.org/ghc.git/blob/7ac22b73b38b60bc26ad2508f57732aa17532a80... here]. I've updated my algorithm. Thanks.
5. h. I was hoping for a little more detail on this skolem business.
A skolem is a type variable that is held distinct from any other type. For example: {{{#!hs nid :: a -> a nid True = False }}} This fails to type-check because, in the body of `nid`, `a` is a skolem. If it were a unification variable, we would just unify `a := Bool`. The "Practical Type Inference" paper has a good discussion of skolems. In a `deriving` clause, any variable quantified in the clause is considered to be a skolem. These skolems are basically unrelated, though, to the skolems mentioned in step (i). The skolems in step (i) would come from something like this: {{{#!hs class C (a :: Type) data D k (b :: k) = D deriving C }}} leads to {{{#!hs instance ... => C (D alpha beta) }}} where `alpha` and `beta` are unification variables. Because these variables are unconstrained, we wish to quantify over them, leading to the final instance declaration {{{#!hs instance forall a (b :: a). ... => C (D a b) }}} The `a` and `b` here are the fresh skolems of stem (i). Your example is {{{#!hs class C j (a :: j) data D = D deriving (forall k. C k) }}} Here, we learn that `ki2` (of step (c)) is the skolem `k`. (This is a skolem because user-written variables are skolems, like in the `nid` example.) That is not of the form `... -> Type`, nor is it a unification variable. (I just added the key qualifier "unification" to that step.) So we reject at this point.
Also, does the skolemicity only kick in if you write an explicit
`forall`? Or would the `k` in `data D = D deriving (C k)` also get skolemized? The user-written variables in a `deriving` clause are skolems whether or not they are explicitly quantified. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler