module Goal1_WellTypedness where
{-@AGDA-}
open import Prelude
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Bool : Set where
true : Bool
false : Bool
F : Bool -> Set
F false = Bool
F true = Nat
one : Nat
one = suc zero
two : Nat
two = suc (suc zero)
f : (b : _) -> F b -> Nat
f false false = zero
f false true = one
f true x = two
-- data D : Nat -> Set where
-- mkD : (b : Bool) (x : F b) -> D (f b x)
postulate D : Nat -> Set
postulate mkD : (b : Bool) (x : F b) -> D (f b x)
mutual
MX : Nat -> Set
MX = _
Mb : Nat -> Bool
Mb = _
-- Here we should check
-- (n : Nat) -> ?X n == (x : F (?b 0)) -> D (f (?b 0) x)
-- and get stuck on comparing the domains, but special inference
-- for constructors is overeager and compares the target types,
-- solving
-- ?X : Nat -> Set
-- ?X x := D (f (?b 0) x)
-- Note that the call to f is not well-typed unless we solve the
-- (as yet unsolved) constraint Nat == F (?b 0).
constr1 : (n : Nat) -> MX n
constr1 = mkD (Mb zero)
-- Now we can form other constraints on ?X. This one simplifies to
-- f (Mb 0) 1 == 0 (*)
constr2 : MX one == D zero
constr2 = refl
-- Finally, we pick the wrong solution for ?b, causing (*) to become
-- f false 1 ≡ 0
-- which crashes with an __IMPOSSIBLE__ when we try to reduce the call to f.
solve-b : Mb == (\_ -> false)
solve-b = refl