Skip to content

GHC
GHC
Open
Opened by Anthony Clayden@AntC3
Report abuse New issue

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 instance D Int] is easily solved: the coercion in the dictionary for F enables the result of op to be cast to type b 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.)

Linked issues