> 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
<simo...@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-boun...@haskell.org] On Behalf Of Ryan
> | Scott
> | Sent: 29 March 2016 14:58
> | To: ghc-devs@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@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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
