Re: instantiating visible parameters in when deriving instances

29 Mar 2016

      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] http://git.haskell.org/ghc.git/blob/b0ab8db61568305f50947058fc5573e2382c84eb...
[2] https://ghc.haskell.org/trac/ghc/ticket/8865

Re: instantiating visible parameters in when deriving instances

Ryan Scott