When does GHC quantify over variables fully determined by fundeps?
Consider the following example:
{-# LANGUAGE FlexibleContexts, FunctionalDependencies, NoMonomorphismRestriction #-}
data AB a b = AB
class C a b | a -> b where
meth :: AB a b -> b
ab :: AB Int b
ab = AB
--foo :: C Int b => b
foo = meth ab
GHC is able to infer the commented type for foo
. Some other test cases which present the same behaviour are tc231
where we have
data Z a = ...
data Q s a chain = ...
class Zork s a b | a -> b where ...
where GHC will infer the following type for foo
:
foo :: Zork s (Z [Char]) b => Q s (Z [Char]) chain -> ST s ()
foo = ...
and tcfail093
, where we have
class Call c h | c -> h where ...
and GHC will infer the following type for dup
:
dup :: Call (IO Int) h => () -> Int -> h
dup = ...
@rae's patch to remove Deriveds changes all these programs to throw type errors. So for the first one we get:
* No instance for (C Int b0) arising from a use of `meth'
* In the expression: meth ab
In an equation for `foo': foo = meth ab
|
12 | foo = meth ab
| ^^^^^^^
for tc231
we get:
* No instance for (Zork s (Z [Char]) b0)
arising from a use of `huh'
* In the expression: huh (s b)
In an equation for `foo': foo b = huh (s b)
and for tcfail093
we get:
* No instance for (Call (IO Int) h0) arising from a use of `call'
* In the expression: call primDup
In an equation for `dup': dup () = call primDup
Pinging @simonpj for thoughts, as Simon committed a change that allowed tc231
and tcfail093
to both typecheck, justified by the (now removed) Note [Important subtlety in oclose]. That note remarks that cases such as tcfail093
are "right on the borderline", so it seems reasonable to revert back to throwing an error.