instantiating visible parameters in when deriving instances
Ryan Scott
ryan.gl.scott at gmail.com
Tue Mar 29 13:58:05 UTC 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:/compiler/typecheck/TcDeriv.hs#l653
[2] https://ghc.haskell.org/trac/ghc/ticket/8865
More information about the ghc-devs
mailing list