Opened 3 years ago

Last modified 22 months ago

#404 new bug

Need to freshen names of type vars when elaborating local sigs.

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


With this example from the Data.Map.Fun, the local binding uses 'elem' as a typevar, but elaboration tries to add another binder for 'elem' in the enclosing function. We cannot shadow type variables, so the program does not type check. Shifting the local fun to a top-level one makes it work.

        (size:    Nat)
        (lookup:  Nat -> elem)
        : Map Fun Nat elem
 = MkMap Fun (mapFun_fromIndexed_fold' size lookup) lookup'
        lookup' ix
         | ix >= size   = Nothing
         | otherwise    = Just (lookup ix)

                [acc elem: Data] 
                (size:   Nat)
                (lookup: Nat -> elem) 
                (f: Nat -> elem -> acc -> acc) (z: acc): acc
         = go 0 z
         where  go ix acc
                  | ix >= size = acc
                  | otherwise  = go (ix + 1) (f ix (lookup ix) acc)

Change History (3)

comment:1 Changed 2 years ago by benl

  • Milestone 0.4.3 deleted

comment:2 Changed 22 months ago by benl

  • Type changed from defect to bug

comment:3 Changed 22 months ago by benl

  • Component changed from Source to Core Translation to Source to Core
Note: See TracTickets for help on using tickets.