unison/unison-src/errors/map-traverse3.u

--map/traverse
structural ability Noop where
  noop : a -> {Noop} a

structural type List a = Nil | Cons a (List a)

map : (a ->{} b) -> List a -> List b
map f = cases
  List.Nil -> List.Nil
  List.Cons h t -> List.Cons (f h) (map f t)

c = List.Cons

z : ∀ a . List a
z = List.Nil

ex = c 1 (c 2 (c 3 z))

pureMap : List Text
pureMap = map (a -> "hello") ex

-- this should not typecheck because map is annotated to take a pure function
zappy : '{Noop} (List Nat)
zappy = 'let map (zap -> Noop.noop (zap Nat.+ 1)) ex

pureMap