System FC for FunDeps: not doing what it says on the tin
Consider this example from the 2011 paper 'System F with Type Equality Coercions', section 2.3 discussing FunDeps
class F a b | a -> b
instance F Int Bool
class D a where { op :: F a b => a -> b }
instance D Int where { op _ = True }
The paper says
Using FC, this problem [of typing the definition of
op
in the instanceD Int
] is easily solved: the coercion in the dictionary forF
enables the result ofop
to be cast to typeb
as required.
I get (I'm at GHC 8.6.1, on a Windows machine)
* Couldn't match expected type `b' with actual type `Bool'
`b' is a rigid type variable bound by
the type signature for:
op :: forall b. F Int b => Int -> b
* In the expression: True
In an equation for `op': op _ = True
In the instance declaration for `D Int'
* Relevant bindings include
op :: Int -> b
(I have a real-life example where I bumped into this rejection.)