instantiating visible parameters in when deriving instances

[Simon Peyton Jones]

|  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