Ticket #73 (new defect)

Opened 6 years ago

Last modified 5 years ago

Bad core generated for recursive function with projections

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

Description

Added by Jared

This function

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

Causes

        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

Changed 5 years ago by benl

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

example
 = 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.

Note: See TracTickets for help on using tickets.