Prove unification correct.

4 files changed, 315 insertions, 46 deletions

diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index 459cb8f..c9fea96 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -85,3 +85,8 @@ appNothingInverse :
   Either (IsNothing f) (IsNothing x)
 appNothingInverse Nothing x prf = Left ItIsNothing
 appNothingInverse (Just f) Nothing prf = Right ItIsNothing
+
+%inline
+export
+bindNothing : {x : Maybe a} -> (0 ok : IsNothing x) -> (f : a -> Maybe b) -> IsNothing (x >>= f)
+bindNothing ItIsNothing f = ItIsNothing
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index ebb7b00..b65859e 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,7 +1,8 @@
 module Data.Term
 
-import public Data.Vect
+import public Data.DPair
 import public Data.Fin.Strong
+import public Data.Vect
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
 
@@ -16,6 +17,10 @@ record Signature where
 %name Signature sig
 
 public export
+(.Op) : Signature -> Type
+sig .Op = Exists sig.Operator
+
+public export
 data Term : Signature -> Nat -> Type where
   Var : SFin (S n) -> Term sig (S n)
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
@@ -99,6 +104,12 @@ opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
 opInjectiveLen Refl = Refl
 
 export
+opInjectiveOp :
+  (prf : Op {sig, k} op ts = Op {sig, k = n} op' us) ->
+  the sig.Op (Evidence k op) = Evidence n op'
+opInjectiveOp Refl = Refl
+
+export
 opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
 opInjectiveTs' Refl = Refl
 
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 1fa53cd..bed4e49 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -2,8 +2,8 @@ module Data.Term.Property
 
 import Data.Term
 
+import public Data.Vect.Quantifiers
 import Data.Vect.Properties.Index
-import Data.Vect.Quantifiers
 import Data.Vect.Quantifiers.Extra
 
 import Syntax.PreorderReasoning
@@ -37,6 +37,10 @@ public export
 All : Vect n (Property sig k) -> Property sig k
 All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong cong))
 
+public export
+UnifiesAll : Vect n (Term sig k) -> Vect n (Term sig k) -> Property sig k
+UnifiesAll ts us = All (zipWith Unifies ts us)
+
 -- Equivalence -----------------------------------------------------------------
 
 public export
@@ -48,40 +52,46 @@ record (<=>) (p, q : Property sig k) where
 -- Properties
 
 export
+Reflexive (Property sig k) (<=>) where
+  reflexive = MkEquivalence (\_ => id) (\_ => id)
+
+export
+Symmetric (Property sig k) (<=>) where
+  symmetric prf = MkEquivalence prf.rightToLeft prf.leftToRight
+
+export
 unifiesSym : (0 t, u : Term sig k) -> Unifies t u <=> Unifies u t
 unifiesSym t u = MkEquivalence (\_, prf => sym prf) (\_, prf => sym prf)
 
 export
 unifiesOp :
-  {k : Nat} ->
-  {0 op : sig.Operator k} ->
-  {0 ts, us : Vect k (Term sig j)} ->
-  Unifies (Op op ts) (Op op us) <=> All (tabulate (\i => Unifies (index i ts) (index i us)))
-unifiesOp = MkEquivalence
-  { leftToRight = \f, prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight f prf)
-  , rightToLeft = \f, prf => irrelevantEq $ cong (Op op) $ rightToLeft f prf
+  {0 k : Nat} ->
+  (0 op : sig.Operator k) ->
+  (ts, us : Vect k (Term sig j)) ->
+  Unifies (Op op ts) (Op op us) <=> UnifiesAll ts us
+unifiesOp op ts us = MkEquivalence
+  { leftToRight = \f, prf => leftToRight ts us f (opInjectiveTs' prf)
+  , rightToLeft = \f, prf => cong (Op op) $ rightToLeft ts us f prf
   }
   where
   leftToRight :
-    (f : SFin j -> Term sig n) ->
-    (Unifies (Op op ts) (Op op us)).Prop f ->
-    (i : _) ->
-    f <$> index i ts = f <$> index i us
-  leftToRight f prf i =
-    Calc $
-      |~ f <$> index i ts
-      ~~ index i (map (f <$>) ts) ...(sym $ indexNaturality i (f <$>) ts)
-      ~~ index i (map (f <$>) us) ...(cong (index i) $ opInjectiveTs' prf)
-      ~~ f <$> index i us         ...(indexNaturality i (f <$>) us)
+    forall k.
+    (ts, us : Vect k (Term sig j)) ->
+    (0 f : (SFin j -> Term sig n)) ->
+    map (f <$>) ts = map (f <$>) us ->
+    (UnifiesAll ts us).Prop f
+  leftToRight [] [] f prf = []
+  leftToRight (t :: ts) (u :: us) f prf =
+    fst (biinj (::) prf) :: leftToRight ts us f (snd $ biinj (::) prf)
 
   rightToLeft :
-    {k : Nat} ->
-    (f : SFin j -> Term sig n) ->
-    {ts, us : Vect k (Term sig j)} ->
-    (All (tabulate (\i => Unifies (index i ts) (index i us)))).Prop f ->
+    forall k.
+    (ts, us : Vect k (Term sig j)) ->
+    (0 f : (SFin j -> Term sig n)) ->
+    (UnifiesAll ts us).Prop f ->
     map (f <$>) ts = map (f <$>) us
-  rightToLeft f {ts = [], us = []} [] = Refl
-  rightToLeft f {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft f prfs)
+  rightToLeft [] [] f [] = Refl
+  rightToLeft (t :: ts) (u :: us) f (prf :: prfs) = cong2 (::) prf (rightToLeft ts us f prfs)
 
 -- Nothing ---------------------------------------------------------------------
 
@@ -111,7 +121,21 @@ nothingExtends : Nothing p -> Nothing (Extension p f)
 nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
-extendCong : (f : _) -> p <=> q -> Extension p f <=> Extension q f
+extendCong2 :
+  {f, g : SFin n -> Term sig k} ->
+  {p, q : Property sig n} ->
+  f .=. g ->
+  p <=> q ->
+  Extension p f <=> Extension q g
+extendCong2 prf1 prf2 = MkEquivalence
+  (\h, x => prf2.leftToRight (h . g) $ p.cong (\i => cong (h <$>) $ prf1 i) x)
+  (\h, x => prf2.rightToLeft (h . f) $ q.cong (\i => sym $ cong (h <$>) $ prf1 i) x)
+
+export
+extendCong :
+  (f : SFin n -> Term sig k) ->
+  p <=> q ->
+  Extension p f <=> Extension q f
 extendCong f prf = MkEquivalence
   (\g => prf.leftToRight (g . f))
   (\g => prf.rightToLeft (g . f))
@@ -154,6 +178,21 @@ extendUnify t u f g =
       ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
       ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))
 
+export
+extendUnifyAll :
+  (ts, us : Vect n (Term sig j)) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
+  Extension (UnifiesAll ts us) (g . f) <=>
+  Extension (UnifiesAll (map (f <$>) ts) (map (f <$>) us)) g
+extendUnifyAll [] [] f g = MkEquivalence (\h, [] => []) (\h, [] => [])
+extendUnifyAll (t :: ts) (u :: us) f g =
+  let head = extendUnify t u f g in
+  let tail = extendUnifyAll ts us f g in
+  MkEquivalence
+    (\h, (x :: xs) => head.leftToRight h x :: tail.leftToRight h xs)
+    (\h, (x :: xs) => head.rightToLeft h x :: tail.rightToLeft h xs)
+
 -- Ordering --------------------------------------------------------------------
 
 public export
@@ -234,27 +273,28 @@ maxCong prf = MkEquivalence
 
 -- Downward Closed -------------------------------------------------------------
 
-public export 0
-DClosed : Property sig k -> Type
-DClosed p =
-  forall m, n.
-  (f : SFin k -> Term sig m) ->
-  (g : SFin k -> Term sig n) ->
-  f <= g ->
-  p.Prop g ->
-  p.Prop f
+public export
+record DClosed (p : Property sig k) where
+  constructor MkDClosed
+  closed :
+    forall m, n.
+    (f : SFin k -> Term sig m) ->
+    (g : SFin k -> Term sig n) ->
+    f <= g ->
+    p.Prop g ->
+    p.Prop f
 
 -- Properties
 
 export
 unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
-unifiesDClosed t u f g prf1 prf2 = Calc $
+unifiesDClosed t u = MkDClosed (\f, g, prf1, prf2 => Calc $
   |~ f <$> t
   ~~ (prf1.sub . g) <$> t ...(subCong prf1.prf t)
   ~~ prf1.sub <$> g <$> t ...(subAssoc prf1.sub g t)
   ~~ prf1.sub <$> g <$> u ...(cong (prf1.sub <$>) prf2)
   ~~ (prf1.sub . g) <$> u ..<(subAssoc prf1.sub g u)
-  ~~ f <$> u              ..<(subCong prf1.prf u)
+  ~~ f <$> u              ..<(subCong prf1.prf u))
 
 export
 optimistLemma :
@@ -266,8 +306,8 @@ optimistLemma :
   (Max (Extension p a)).Prop f ->
   (Max (Extension (All ps) (f . a))).Prop g ->
   (Max (Extension (All (p :: ps)) a)).Prop (g . f)
-optimistLemma closed (x, max1) (y, max2) =
-  ( ( closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x
+optimistLemma prf (x, max1) (y, max2) =
+  ( ( prf.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x
     :: (All ps).cong (\i => sym $ subAssoc g f (a i)) y
     )
   , \h, (x' :: y') =>
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 35cc048..f75a61a 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -208,8 +208,25 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $
   ~~ (eval sub2 . eval sub1) <$> (t `for` x) i ...(subCong (evalHomo sub2 sub1) ((t `for` x) i))
   ~~ eval sub2 <$> eval sub1 <$> (t `for` x) i ...(subAssoc (eval sub2) (eval sub1) ((t `for` x) i))
 
+export
+appendUnitLeft : (sub : AList sig k n) -> [<] ++ sub = sub
+appendUnitLeft [<] = Refl
+appendUnitLeft (sub :< tx) = cong (:< tx) (appendUnitLeft sub)
+
+export
+appendAssoc :
+  (sub3 : AList sig _ _) ->
+  (sub2 : AList sig _ _) ->
+  (sub1 : AList sig _ _) ->
+  sub3 ++ (sub2 ++ sub1) = (sub3 ++ sub2) ++ sub1
+appendAssoc sub3 sub2 [<] = Refl
+appendAssoc sub3 sub2 (sub1 :< tx) = cong (:< tx) (appendAssoc sub3 sub2 sub1)
+
 -- Unification -----------------------------------------------------------------
 
+coerce : {0 op, op' : sig.Op} -> op = op' -> Vect op'.fst a -> Vect op.fst a
+coerce Refl = id
+
 flexFlex : SFin (S n) -> SFin (S n) -> Exists (AList sig (S n))
 flexFlex x y = case thick x y of
   Just z => Evidence _ [<(Var' z, x)]
@@ -222,20 +239,19 @@ flexRigid x t = case check x t of
 
 export
 amgu :
-  DecEq (Exists sig.Operator) =>
+  DecEq sig.Op =>
   (t, u : Term sig n) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 amguAll :
-  DecEq (Exists sig.Operator) =>
+  DecEq sig.Op =>
   (ts, us : Vect k (Term sig n)) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 
-amgu (Op op ts) (Op op' us) acc =
-  case decEq {t = Exists sig.Operator} (Evidence _ op) (Evidence _ op') of
-    Yes prf => amguAll ts (replace {p = \k => Vect k (Term sig n)} (sym $ cong fst prf) us) acc
-    No neq => Nothing
+amgu (Op op ts) (Op op' us) acc with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op'))
+  amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
+  _ | No neq = Nothing
 amgu (Var x) (Var y) (Evidence _ [<]) = Just (flexFlex x y)
 amgu (Var x) (Op op' us) (Evidence _ [<]) = flexRigid x (Op op' us)
 amgu (Op op ts) (Var y) (Evidence _ [<]) = flexRigid y (Op op ts)
@@ -252,7 +268,7 @@ amguAll (t :: ts) (u :: us) acc = do
   amguAll ts us acc
 
 export
-mgu : DecEq (Exists sig.Operator) => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecEq sig.Op => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
 mgu t u = amgu t u (Evidence _ [<])
 
 -- Properties
@@ -347,3 +363,200 @@ stepEquiv :
   Extension (Unifies t u) (eval (sub :< (v, x))) <=>
   Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub)
 stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub)
+
+parameters {auto _ : DecEq sig.Op}
+  public export
+  data AmguProof : (t, u : Term sig k) -> Exists (AList sig k) -> Type where
+    Success :
+      {0 sub : Exists (AList sig k)} ->
+      (sub' : Exists (AList sig sub.fst)) ->
+      (Max (Extension (Unifies t u) (eval sub.snd))).Prop (eval sub'.snd) ->
+      amgu t u sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
+      AmguProof t u sub
+    Failure :
+      {0 sub : Exists (AList sig k)} ->
+      Nothing (Extension (Unifies t u) (eval sub.snd)) ->
+      IsNothing (amgu t u sub) ->
+      AmguProof t u sub
+
+  public export
+  data AmguAllProof : (ts, us : Vect n (Term sig k)) -> Exists (AList sig k) -> Type where
+    SuccessAll :
+      {0 sub : Exists (AList sig k)} ->
+      (sub' : Exists (AList sig sub.fst)) ->
+      (Max (Extension (UnifiesAll ts us) (eval sub.snd))).Prop (eval sub'.snd) ->
+      amguAll ts us sub = Just (Evidence sub'.fst (sub'.snd ++ sub.snd)) ->
+      AmguAllProof ts us sub
+    FailureAll :
+      {0 sub : Exists (AList sig k)} ->
+      Nothing (Extension (UnifiesAll ts us) (eval sub.snd)) ->
+      IsNothing (amguAll ts us sub) ->
+      AmguAllProof ts us sub
+
+export
+amguProof :
+  DecEq sig.Op =>
+  (t, u : Term sig n) ->
+  (sub : Exists (AList sig n)) ->
+  AmguProof t u sub
+export
+amguAllProof :
+  DecEq sig.Op =>
+  (ts, us : Vect k (Term sig n)) ->
+  (sub : Exists (AList sig n)) ->
+  AmguAllProof ts us sub
+
+amguProof (Op op ts) (Op op' us) sub
+  with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op')) proof prf
+  amguProof (Op op ts) (Op op us) sub | Yes Refl
+    with (amguAllProof ts us sub)
+    _ | SuccessAll sub' val prf' =
+      let
+        cong :
+          Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub.snd)) <=>
+          Max (Extension (UnifiesAll ts us) (eval sub.snd))
+        cong = maxCong $ extendCong (eval sub.snd) $ unifiesOp op ts us
+      in
+      Success sub'
+        (cong.rightToLeft (eval sub'.snd) val)
+        (rewrite prf in prf')
+    _ | FailureAll absurd prf' =
+      Failure
+        (nothingEquiv (symmetric $ extendCong (eval sub.snd) $ unifiesOp op ts us) absurd)
+        (rewrite prf in prf')
+  _ | No neq =
+    Failure
+      (\f, prf => neq $ opInjectiveOp prf)
+      (rewrite prf in ItIsNothing)
+amguProof (Var x) (Var y) (Evidence _ [<]) with (thick x y) proof prf
+  _ | Just z = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
+  _ | Nothing = Success (flexFlex x y) (flexFlexUnifies x y) (rewrite prf in Refl)
+amguProof (Var x) (Op op' us) (Evidence _ [<]) with (flexRigid x (Op op' us)) proof prf
+  _ | Just sub@(Evidence _ _) = Success sub (flexRigidUnifies x (Op op' us) prf) prf
+  _ | Nothing =
+    Failure
+      (flexRigidFails x op' us (rewrite prf in ItIsNothing))
+      (rewrite prf in ItIsNothing)
+amguProof (Op op ts) (Var y) (Evidence _ [<]) with (flexRigid y (Op op ts)) proof prf
+  _ | Just sub@(Evidence _ sub') =
+    let
+      cong :
+        Max (Extension (Unifies (Var y) (Op op ts)) Var') <=>
+        Max (Extension (Unifies (Op op ts) (Var y)) Var')
+      cong = maxCong $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+    in
+    Success sub
+      (cong.leftToRight (eval sub.snd) (flexRigidUnifies y (Op op ts) prf))
+      prf
+  _ | Nothing =
+    let
+      cong :
+        Nothing (Extension (Unifies (Var y) (Op op ts)) Var') ->
+        Nothing (Extension (Unifies (Op op ts) (Var y)) Var')
+      cong = nothingEquiv $ extendCong Var' $ unifiesSym (Var y) (Op op ts)
+    in
+    Failure
+      (cong $ flexRigidFails y op ts (rewrite prf in ItIsNothing))
+      (rewrite prf in ItIsNothing)
+amguProof (Var x) (Var y) (Evidence l (sub :< (v, z)))
+  with (amguProof ((v `for` z) x) ((v `for` z) y) (Evidence _ sub))
+  _ | Success sub' val prf =
+    let
+      cong' :
+        Max (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
+        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
+      cong' = maxCong $ stepEquiv (Var x) (Var y) sub v z
+    in
+    Success sub'
+      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong (map (:< (v, z))) prf)
+  _ | Failure absurd prf =
+    Failure
+      (nothingEquiv (symmetric $ stepEquiv (Var x) (Var y) sub v z) absurd)
+      (mapNothing (:< (v, z)) prf)
+amguProof (Var x) (Op op' us) (Evidence _ (sub :< (v, z)))
+  with (amguProof ((v `for` z) x) ((v `for` z) <$> Op op' us) (Evidence _ sub))
+  _ | Success sub' val prf =
+    let
+      cong' :
+        Max (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
+        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
+      cong' = maxCong $ stepEquiv (Var x) (Op op' us) sub v z
+    in
+    Success sub'
+      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong (map (:< (v, z))) prf)
+  _ | Failure absurd prf =
+    Failure
+      (nothingEquiv (symmetric $ stepEquiv (Var x) (Op op' us) sub v z) absurd)
+      (mapNothing (:< (v, z)) prf)
+amguProof (Op op ts) (Var y) (Evidence _ (sub :< (v, z)))
+  with (amguProof ((v `for` z) <$> Op op ts) ((v `for` z) y) (Evidence _ sub))
+  _ | Success sub' val prf =
+    let
+      cong' :
+        Max (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
+        Max (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
+      cong' = maxCong $ stepEquiv (Op op ts) (Var y) sub v z
+    in
+    Success sub'
+      (cong'.rightToLeft (eval sub'.snd) val)
+      (cong (map (:< (v, z))) prf)
+  _ | Failure absurd prf =
+    Failure
+      (nothingEquiv (symmetric $ stepEquiv (Op op ts) (Var y) sub v z) absurd)
+      (mapNothing (:< (v, z)) prf)
+
+amguAllProof [] [] (Evidence _ sub) =
+  SuccessAll (Evidence _ [<])
+    ([], \g, x => varMax g)
+    (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
+amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
+  _ | Success sub' val prf with (amguAllProof ts us (Evidence _ (sub'.snd ++ sub.snd)))
+    _ | SuccessAll sub'' val' prf' =
+      let
+        cong' =
+          maxCong $
+          extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+        opt =
+          optimistLemma (unifiesDClosed t u) val $
+          cong'.leftToRight (eval sub''.snd) val'
+      in
+      SuccessAll (Evidence _ (sub''.snd ++ sub'.snd))
+        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub.snd))).cong
+          (\i => sym $ evalHomo sub''.snd sub'.snd i)
+          opt)
+        (rewrite prf in rewrite prf' in
+          cong (\sub => Just (Evidence sub''.fst sub)) $
+          appendAssoc sub''.snd sub'.snd sub.snd)
+    _ | FailureAll absurd prf' =
+      let
+        cong' = extendCong2 (evalHomo sub'.snd sub.snd) (reflexive {x = UnifiesAll ts us})
+      in
+      FailureAll
+        (failTail val $ nothingEquiv cong' absurd)
+        (rewrite prf in prf')
+  _ | Failure absurd prf =
+    FailureAll
+      (failHead absurd)
+      (bindNothing prf (amguAll ts us))
+
+parameters {auto _ : DecEq sig.Op}
+  namespace MguProof
+    public export
+    data MguProof : (t, u : Term sig k) -> Type where
+      Success :
+        (sub : Exists (AList sig k)) ->
+        (Max (Unifies t u)).Prop (eval sub.snd) ->
+        mgu t u = Just sub ->
+        MguProof t u
+      Failure :
+        Nothing (Unifies t u) ->
+        IsNothing (mgu t u) ->
+        MguProof t u
+
+export
+mguProof : DecEq sig.Op => (t, u : Term sig k) -> MguProof t u
+mguProof t u with (amguProof t u (Evidence _ [<]))
+  _ | Success (Evidence _ sub) val prf = Success (Evidence _ sub) val prf
+  _ | Failure absurd prf = Failure absurd prf