Poor interaction between functional dependencies and partial type signatures
Summary
A fundep is surprisingly unable to fill in a partial type signature
Steps to reproduce
{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #-}
infixr 6 :::
data HList xs where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
class AppHList ts o f | ts f -> o, ts o -> f where
appHList :: f -> HList ts -> o
instance AppHList '[] o o where
appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
appHList f (x ::: xs) = appHList (f x) xs
foo :: (a -> b -> c) -> HList '[a, b] -> _
foo = appHList
This fails with
AbstractList.hs:35:7: error:
• Couldn't match type ‘c’ with ‘w0’
arising from a functional dependency between:
constraint ‘AppHList '[] w0 c’ arising from a use of ‘appHList’
instance ‘AppHList '[] o o’ at AbstractList.hs:29:10-25
‘c’ is a rigid type variable bound by
the inferred type of foo :: (a -> b -> c) -> HList '[a, b] -> w0
at AbstractList.hs:35:1-14
• In the expression: appHList
In an equation for ‘foo’: foo = appHList
• Relevant bindings include
foo :: (a -> b -> c) -> HList '[a, b] -> w0
(bound at AbstractList.hs:35:1)
Expected behavior
I'd expect GHC to fill in _
with c
. Indeed, if I leave out the type signature and write
foo (f :: a -> b -> c) (args :: HList '[a, b]) = appHList f args
then GHC correctly infers foo :: (a -> b -> c) -> HList '[a, b] -> c
.
Environment
- GHC version used: 8.6.3
Optional:
- Operating System:
- System Architecture: