Opened 10 years ago

Closed 10 years ago

Last modified 7 years ago

#84 closed defect (fixed)

Fix postgeneralisation check.

Reported by: benl Owned by:
Priority: blocker Milestone:
Component: Source Type Inferencer Version: 0.1.2
Keywords: Cc:


Testcase is Error/Closure/LateExport?

main ()
 = do   ref     = Ref id
        f       = \x -> ref.x
        ref#x   #= succ
        f () "oh noes"

Adding the type scheme for f back to the graph overwrites the original fn constructor there, so we can't sensibly extract the type and re-generalise.

Need to store complete type schemes in a separate table, or in the graph in a way that doesn't prevent us from extracting and generalising types again.

The error in above program would have been detected before we started trimming type constructors out of closures. After inference, the type of f would have been

f :: forall a. () -(e1 c1)> a -> a
  :- e1 = Read r1
  ,  c1 = ref : forall b. Ref r1 (b -> b)
  ,  Mutable r1

As r1 is mutable, the fact that b is quantified in the constraint for c1 tells us that the scheme is bad. However, trimming constructors like Ref out of types gives:

f :: forall a. () -(e1 c1)> a -> a
  :- e1 = Read r1
  ,  c1 = ref : r1

This is valid if r1 is really constant. But if it's not then we've lost the forall b. (b -> b) part, can't do the simpler check, and have to do a complete re-extract and re-generalise instead.

Change History (2)

comment:1 Changed 10 years ago by benl

  • Resolution set to fixed
  • Status changed from new to closed

comment:2 Changed 7 years ago by benl

  • Milestone 0.1.3 deleted

Milestone 0.1.3 deleted

Note: See TracTickets for help on using tickets.