Failure.agda

module Failure where

data Bool : Set where
  false : Bool
  true  : Bool

if_then_else_ : {A B : Set} → (x : Bool) → A → B → (λ {true → A ; false → B}) x
if true then x else _ = x
if false then _ else x = x

{-
You need to fix the following errors before you can compile
the module:

Failed to solve the following constraints:
  _15 := λ {.A} {.B} .x x → x [blocked on problem 11]
  [11] .B =< _12 false : Set
  Set = _6 false
  _13 := λ {.A} {.B} x .x → x [blocked on problem 8]
  [8] .A =< _12 true : Set
  Set = _6 true
  _11 := (_ : _8 x) [x] :? _6 x
  _9 := λ { true → A ; false → B } :? _8 x

-}