Opened 2 months ago

#404 new defect

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

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

Description

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.

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

        mapFun_fromIndexed_fold'
                [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 (0)

Note: See TracTickets for help on using tickets.