instantiating visible parameters in when deriving instances

[Ryan Scott]

> Why should it make a difference whether it's visible or not.  Can't we behave the same for both?

Oops, I made the wrong distinction. I should have said: we freely
unify eta-reduced type parameters when deriving, but if a type
parameter isn't eta-reduced, then we generate equality constraints
instead of unifying it.

That is, the distinction between

    instance Functor P1
    -- with -fprint-explicit-kinds, this would be instance Functor * P1

and

    instance (k ~ *) => Functor (P2 k)

We can't generate equality constraints for eta-reduced type variables
since there's literally no way to refer to them in an instance.

Ryan S.

On Tue, Mar 29, 2016 at 10:47 AM, Simon Peyton Jones
<simonpj at microsoft.com> wrote:
> |  So I'm starting to lean towards Simon's proposal. That is, we freely
> |  unify non-visible type parameters when deriving, but if a type
> |  parameter is visible, then we generate equality constraints instead of
> |  unifying it.
>
> Why should it make a difference whether it's visible or not.  Can't we behave the same for both?
>
> Simon
>
>
> |  -----Original Message-----
> |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Ryan
> |  Scott
> |  Sent: 29 March 2016 14:58
> |  To: ghc-devs at haskell.org
> |  Subject: Re: instantiating visible parameters in when deriving
> |  instances
> |
> |  Simon, did you meant P2? (Since you can't write instance (k ~ *) =>
> |  Functor (P1 (a :: k)), as that's ill-kinded). Something like this?
> |
> |      data P2 k (a :: k) = MkP2
> |      instance (k ~ *) => Functor (P2 k)
> |
> |  That's an interesting idea. Be aware that you actually can't compile
> |  that code at the moment, since GHC complains:
> |
> |      * Expected kind ‘* -> *’, but ‘P2 k’ has kind ‘k -> *’
> |      * In the first argument of ‘Functor’, namely ‘P2 k’
> |        In the instance declaration for ‘Functor (P2 k)’
> |
> |  I hope this is a bug and not a fundamental limitation.
> |
> |  There's another wrinkle in the design we must consider. Not only can
> |  datatypes have dependent type parameters, but so can typeclasses
> |  themselves. Consider:
> |
> |      {-# LANGUAGE FlexibleInstances #-}
> |      {-# LANGUAGE GeneralizedNewtypeDeriving #-}
> |      {-# LANGUAGE MultiParamTypeClasses #-}
> |      {-# LANGUAGE TypeInType #-}
> |      module Cat where
> |
> |      import Data.Kind
> |
> |      class Cat k (cat :: k -> k -> *) where
> |        catId   :: cat a a
> |        catComp :: cat b c -> cat a b -> cat a c
> |
> |      instance Cat * (->) where
> |        catId   = id
> |        catComp = (.)
> |
> |      newtype Fun a b = Fun (a -> b) deriving (Cat k)
> |
> |  I was surprised to find out that this code currently compiles without
> |  issue on GHC 8.0, even though we're deriving (Cat k) instead of (Cat
> |  *). This is an effect of the way GHC currently handles deriving
> |  clauses, since it unifies the kind of the datatype and typeclass
> |  beforehand (therefore, it silently gets unified to Cat * before
> |  generating the instance). [1]
> |
> |  Is this correct? It definitely feels a bit off. We currently allow this
> |  (see Trac #8865 [2]):
> |
> |      newtype T a b = MkT (Either a b) deriving ( Category )
> |
> |  Even though Category :: k -> k -> * (i.e., we silently unify k with *).
> |  The difference here, as is the difference between P1 and P2 in Simon's
> |  email, is that k is not visible, so it's out-of-sight and out-of-mind.
> |  When k is visible, as in Cat, when now must be conscious of how it's
> |  used in a deriving clause.
> |
> |  The Cat code is lying in the sense that we aren't deriving an instance
> |  that begins with (Cat k), but rather:
> |
> |      instance Cat * Fun where ...
> |
> |  Using Simon's advice, we could just as well generate:
> |
> |      instance (k ~ *) => Cat k Fun where ...
> |
> |  (Again, this doesn't currently compile on 8.0. I really hope that's
> |  just a bug.)
> |
> |  So I'm starting to lean towards Simon's proposal. That is, we freely
> |  unify non-visible type parameters when deriving, but if a type
> |  parameter is visible, then we generate equality constraints instead of
> |  unifying it.
> |
> |  Ryan S.
> |  -----
> |  [1]
> |  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fgit.has
> |  kell.org%2fghc.git%2fblob%2fb0ab8db61568305f50947058fc5573e2382c84eb%3a
> |  %2fcompiler%2ftypecheck%2fTcDeriv.hs%23l653&data=01%7c01%7csimonpj%4006
> |  4d.mgd.microsoft.com%7cdd343f6279d74b40a30b08d357da348e%7c72f988bf86f14
> |  1af91ab2d7cd011db47%7c1&sdata=I2YgFKCYkZtpSJlN7UzOyawgK2LncTQIlE2PpOAwP
> |  2c%3d
> |  [2] https://ghc.haskell.org/trac/ghc/ticket/8865
> |  _______________________________________________
> |  ghc-devs mailing list
> |  ghc-devs at haskell.org
> |  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.ha
> |  skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> |  devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd343f6279d74
> |  b40a30b08d357da348e%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=19EhLy
> |  AsemDkPIdmK08C0XBbLufiKEsEwYuLqWhCH3s%3d