Opened 11 years ago

Closed 7 years ago

#73 closed defect (wontfix)

Bad core generated for recursive function with projections

Reported by: benl Owned by:
Priority: normal Milestone:
Component: Source to Core Translation Version: 0.1.2
Keywords: Cc:


Added by Jared

This function

example = []
  where xs = example
        y  = xs.head


        applyTypeT: Kind error in type application.
            caller = Just Core.Bind.bindXDo
            in application:
                (\/ (y :: *) -> ...) (Const %rTS1)
                type: Const %rTS1
            has kind: Just Const %rTS1
            expected: *

Test is T73-BadCoreProj

Change History (3)

comment:1 Changed 10 years ago by benl

This should probably give an ambiguous projection error. Desugaring the example gives:

 = let xs = example
       y  = xs.head
   in  []

The type inferencer examines the bindings one at a time, and when it comes to resolve the xs.head projection it won't know that xs is a list yet.

It would be nice to actually assign a type to this, using the fact that (example :: []). However, but there are interactions with the mechanism that reorders bindings during inference, the solver is already too complicated, and thinking about it makes my head hurt. We should just reject this program for now, then refactor the solver to make it easier to understand what's going on.

comment:2 Changed 8 years ago by benl

  • Milestone 0.1.3 deleted
  • Priority changed from blocker to normal

comment:3 Changed 7 years ago by benl

  • Resolution set to wontfix
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.