Fundeps and equalities
|Reported by:||simonpj||Owned by:|
|Type of failure:||None/Unknown||Test Case:||indexed-types/should_fail/T4254|
|Related Tickets:||Differential Rev(s):|
Claus asks what behavior these functions should have:
class FD a b | a -> b where op :: a -> b; op = undefined instance FD Int Bool ok1 :: forall a b. (a~Int,FD a b) => a -> b ok1 = op ok2 :: forall a b. (a~Int,FD a b,b~Bool) => a -> Bool ok2 = op fails :: forall a b. (a~Int,FD a b) => a -> Bool fails = op
ok2 typecheck, but
fails doesn't. I think
ok1should fail because it requires the skolem
Bool, but has no way to prove it.
ok1should succeed, because the caller passes in evidence that
failsshould fail for the same reason as
This isn't very high priority, but this ticket is just to make us check in due course that the new type checker does the right thing.