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: