Ticket #84 (closed defect: fixed)

Opened 5 years ago

Last modified 5 years ago

Fix postgeneralisation check.

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

Description

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

Changed 5 years ago by benl

  • status changed from new to closed
  • resolution set to fixed
Note: See TracTickets for help on using tickets.