Agda-2.3.2.2: test/fail/Negative5.agda

module Negative5 where

data Funny (A : Set) : Set where
  funny : A -> Funny (Funny A -> A) -> Funny A