Opened 7 years ago

Closed 6 years ago

#4254 closed bug (fixed)

Fundeps and equalities

Reported by: simonpj Owned by:
Priority: low Milestone: 7.0.1
Component: Compiler Version: 6.12.3
Keywords: Cc: dimitris@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_fail/T4254
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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

In 6.12, ok1 and ok2 typecheck, but fails doesn't. I think

  • ok1 should fail because it requires the skolem b to be Bool, but has no way to prove it.
  • ok1 should succeed, because the caller passes in evidence that b~Bool
  • fails should fail for the same reason as ok1

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.

Change History (3)

comment:1 Changed 7 years ago by igloo

Blocked By: 4232 added

comment:2 Changed 6 years ago by igloo

Blocked By: 4232 removed

comment:3 Changed 6 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T4254

Fine with the new typechecker. ok1 an ok1 pass (which I now think they should), but fails fails (ditto).


Note: See TracTickets for help on using tickets.