packages feed

idris-0.12.3: test/regression002/reg023.idr

module Foo

f : Type -> Type
f x = f x

bad : f Nat
bad = Z