Opened 4 years ago

Closed 4 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 Difficulty:
Test Case: indexed-types/should_fail/T4254 Blocked By:
Blocking: Related Tickets:

Description

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 4 years ago by igloo

  • Blocked By 4232 added

comment:2 Changed 4 years ago by igloo

  • Blocked By 4232 removed

comment:3 Changed 4 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to indexed-types/should_fail/T4254

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

Simon

Note: See TracTickets for help on using tickets.