Confused by type error on expression with consumption

[nbos]

The program

def main = map (const (iota 3 with [0] = 1)) (iota 3)

raises a type error

Cannot apply "map" to "(const (iota 3 with [0] = 1))" (invalid type).
Expected: a₈ -> x₁₀
Actual:   b₇ -> [3]i64

Type
  a₈ -> x₁₀
found to be functional.
When checking type of expression with consumption at test.fut:1:24-42

while

def main = map (\_ -> (iota 3 with [0] = 1)) (iota 3)

raises no such error. It's not clear to me why the first would raise a type error and not the second, or why the expected type can't be instantiated into the actual.

[athas]

It's a conservative check meant to ensure that defunctionalisation can duplicate expressions when needed. This is in general not safe when the expression performs consumption (although it is in this case). It's been a very long while since this rule was instituted, so I no longer remember the actual problematic examples.

[athas]

We can probably relax this a bit. I hope nothing important breaks.