Agda-2.3.2.2: test/fail/ShapeIrrelevantParameterNoBecauseOfRecursion.agda

{-# OPTIONS --experimental-irrelevance #-}
module ShapeIrrelevantParameterNoBecauseOfRecursion where

data ⊥ : Set where
record ⊤ : Set where

data Bool : Set where
  true false : Bool

True : Bool → Set
True false = ⊥
True true  = ⊤

data D ..(b : Bool) : Set where
  c : True b → D b  -- should fail

fromD : {b : Bool} → D b → True b
fromD (c p) = p

cast : .(a b : Bool) → D a → D b
cast _ _ x = x

bot : ⊥
bot = fromD (cast true false (c _))