Refactor DeriveFunctor to handle rank-n field types better
DeriveFunctor
falls over on constructors with sufficiently complicated rank-n field types, such as this one:
data T a = MkT (forall b. b -> (forall c. a -> c) -> a)
deriving Functor
GHC will try to generate the following code for the derived Functor T
instance:
instance Functor T where
fmap f (MkT a1)
= MkT
((\ b7 b8
-> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
(b7 ((\ b1 -> b1) b8)))
a1)
This fails to typecheck with the following error:
Bug.hs:15:12: error:
• Couldn't match type ‘forall c. a -> c’ with ‘a -> p0’
Expected type: b1 -> (a -> p0) -> a
Actual type: b1 -> (forall c. a -> c) -> a
• In the first argument of ‘\ b7 b8
-> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
(b7 ((\ b1 -> b1) b8))’, namely
‘a1’
In the first argument of ‘MkT’, namely
‘((\ b7 b8
-> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
(b7 ((\ b1 -> b1) b8)))
a1)’
In the expression:
MkT
((\ b7 b8
-> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
(b7 ((\ b1 -> b1) b8)))
a1)
• Relevant bindings include
a1 :: forall b. b -> (forall c. a -> c) -> a
(bound at Bug.hs:10:15)
f :: a -> b (bound at Bug.hs:10:8)
fmap :: (a -> b) -> T a -> T b (bound at Bug.hs:10:3)
|
15 | a1)
| ^^
However, it would typecheck if the generated right-hand side were beta-reduced a little bit more:
instance Functor T where
fmap f (MkT g)
= MkT
(\ b8
-> (\ b6 -> f (g b8 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6))))
We should refactor DeriveFunctor
so that it generates this sort of code. Paraphrasing Simon's suggestion from !2600 (comment 256528), here is the current design of $fmap
, the type-driven transformer function that powers DeriveFunctor
's codegen:
$(fmap 'a 'b) = \x -> x -- when b does not contain a
$(fmap 'a 'a) = f
$(fmap 'a '(b1,b2)) = \x -> case x of (x1,x2) -> ($(fmap 'a 'b1) x1, $(fmap 'a 'b2) x2)
$(fmap 'a '(T b1 b2)) = fmap $(fmap 'a 'b2) -- when a only occurs in the last parameter, b2
$(fmap 'a '(b -> c)) = \x b -> $(fmap 'a' 'c) (x ($(cofmap 'a 'b) b))
$(fmap a ty)
produces a term of type ty -> ty[b/a]
. Notice how the case for function types (i.e., $(fmap 'a '(b -> c)) = \x b -> ...
) generates a lambda expression with two arguments, where the first argument x
is a function type. This is exactly the argument we want to beta reduce.
We can accomplish this beta reduction by giving $fmap
an extra argument term (e.g., x1
) along with its type (e.g., ty1
). So in a call $(fmap a ty x)
, we have:
-
There is a precondition that
x :: ty
. -
The call produces a term of type
ty[b/a]
:$(fmap 'a 'b x) = x -- when b does not contain a $(fmap 'a 'a x) = f x $(fmap 'a '(b1,b2) x) = case x of (x1,x2) -> ($(fmap 'a x1 'b1) x1, $(fmap 'a x2 'b2)) $(fmap 'a '(T b1 b2) x) = fmap (\y. $(fmap 'a y 'b2)) x -- when a only occurs in the last parameter, b2 $(fmap 'a '(tb -> tc) x) = \(y:tb[b/a]) -> $(fmap 'a' 'tc' (x $(cofmap 'a 'tb y)))
This was spun off from this discussion, where this idea was proposed as a way to make DeriveFunctor
continue to work on things like data T a = MkT (Int -> forall c. c -> a) deriving Functor
after simplified subsumption is implemented. But this idea can be implemented independently, as it makes more programs typecheck even without the need for simplified subsumption.