Re: [GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

11 Oct 2017

      #14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
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 simonpj):
...
Trying to stick foralls on just C c1 ... cn feels nonsensical,
You could try not thinking of them as foralls.  Say
 {{{
 data D = D deriving ({k a}. C (a :: k))
 }}}
 where I'm using `{k a}` to bring `k` and `a` into scope.

 But they ARE skolems. I'm sure you wouldn't be happy with
 {{{
 data D = D deriving( {a}. C a }
 }}}
 it the derived instance declaration ended up being
 {{{
 instance C Int D
 }}}
 where the `a` gets unified with `Int` somehow.  (Fundeps or something.)
 This quantification is ''per-deriving-clause''.  If you say `a` you mean
 `a` and not `Int`!
...
why the user-written kinds of a data type's type variables don't fall
 under the same scrutiny
Because they are shared across the data type decl itself, ''and'' all the
 deriving clauses. So in
 {{{
 data Proxy k (a :: k) = Proxy deriving(  Functor, ...others... )
 }}}
 the `Functor` instance only makes sense when `k=*`, so we specialise it to
 that
 {{{
   instance GHC.Base.Functor (Main.Proxy *) where
 }}}
 We ''can't'' turn that `k` into `*` in the decl without crippling `Proxy`.

 To put it another way:
 * The kind binders in the data decl belong to the data decl
 * The freshly bound variables in the deriving clause belong to the
 instance decl
 * Naturally, the quantified variables of the data decl may be instantiated
 in the instance decl.

 Does that help?

 Is this essentially the same ticket as #14332?  Can we combine?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler