idris-0.9.9: test/test010/test010a.idr
module main
%default total
data Bad = MkBad (Bad -> Int) Int
| MkBad' Int
bar : Bad
bar = MkBad (\x => 3) 3
module main
%default total
data Bad = MkBad (Bad -> Int) Int
| MkBad' Int
bar : Bad
bar = MkBad (\x => 3) 3