[Agda] Friday afternoon magic

[Nils Anders Danielsson]

Hi,

Some readers of this list may enjoy the following exercise: explain why
"works" type-checks, but "fails" doesn't.

module Magic where

data Bool : Set where
   true false : Bool

data Bool′ (A : Set) : Set where
   true false : Bool′ A

to : (A : Set) → Bool → Bool′ A
to _ true  = true
to _ false = false

from : (A : Set) → Bool′ A → Bool
from _ true  = true
from _ false = false

magic : (A : Set) → Bool → Bool
magic A b = from A (to A b)

f₁ : Bool → Bool → Bool
f₁ false false = true
f₁ _     _     = true

f₂ : Bool → Bool → Bool
f₂ b₁ b₂ = magic Empty (f₁ b₁ b₂)
   where
   data Empty : Set where

data P (f : Bool → Bool → Bool) : (Bool → Bool) → Set where
   p : (b : Bool) → P f (f b)

fails : P f₁ (f₁ false)
fails = p _  -- Unsolved constraint: (f₁ _24 x) = (f₁ false x) : Bool.

works : P f₂ (f₂ false)
works = p _  -- No unsolved constraints.

-- 
/NAD