| 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@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