module Data.Term.Unify

import Data.DPair
import Data.Fin.Occurs
import Data.Fin.Strong
import Data.Maybe.Properties
import Data.Singleton
import Data.Term
import Data.Term.Property
import Data.Term.Zipper

import Decidable.Equality

import Syntax.PreorderReasoning

-- Check -----------------------------------------------------------------------

export
check : SFin k -> Term sig k -> Maybe (Term sig (pred k))
checkAll : SFin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))

check x (Var y) = Var' <$> thick x y
check x (Op op ts) = Op op <$> checkAll x ts

checkAll x [] = Just []
checkAll x (t :: ts) = [| check x t :: checkAll x ts |]

-- Properties

export
checkOccurs :
  (x : SFin k) ->
  (zip : Zipper sig k) ->
  IsNothing (check x (zip + Var' x))
checkAllOccurs :
  (x : SFin k) ->
  (i : SFin n) ->
  (ts : Vect (pred n) (Term sig k)) ->
  (zip : Zipper sig k) ->
  IsNothing (checkAll x (insertAt' i (zip + Var' x) ts))

checkOccurs x Top = mapNothing Var' (thickRefl x)
checkOccurs x (Op op i ts zip) = mapNothing (Op op) (checkAllOccurs x i ts zip)

checkAllOccurs x FZ ts zip =
  appLeftNothingIsNothing
    (appRightNothingIsNothing (Just (::)) (checkOccurs x zip))
    (checkAll x ts)
checkAllOccurs x (FS i) (t :: ts) zip =
  appRightNothingIsNothing
    (Just (::) <*> check x t)
    (checkAllOccurs x i ts zip)

export
checkNothing :
  (x : SFin k) ->
  (t : Term sig k) ->
  (0 _ : IsNothing (check x t)) ->
  (zip : Zipper sig k ** t = zip + Var' x)
checkAllNothing :
  (x : SFin k) ->
  (t : Term sig k) ->
  (ts : Vect n (Term sig k)) ->
  (0 _ : IsNothing (checkAll x (t :: ts))) ->
  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt' i (zip + Var' x) ts')

checkNothing x (Var y) prf =
  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var' (thick x y) prf))))
checkNothing x (Op op (t :: ts)) prf =
  let (i ** ts' ** zip ** prf) = checkAllNothing x t ts (mapNothingInverse (Op op) _ prf) in
  (Op op i ts' zip ** cong (Op op) prf)

checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (checkAll x ts) prf)
  _ | Left prf' = case appNothingInverse (Just (::)) (check x t) prf' of
      Right prf =>
        let (zip ** prf) = checkNothing x t prf in
        (FZ ** ts ** zip ** cong (:: ts) prf)
  checkAllNothing x t (t' :: ts) prf | Right prf' =
    let (i ** ts ** zip ** prf) = checkAllNothing x t' ts prf' in
    (FS i ** t :: ts ** zip ** cong (t ::) prf)

export
checkThin :
  (x : SFin (S k)) ->
  (t : Term sig k) ->
  IsJust (check x (pure (thin x) <$> t))
checkAllThin :
  (x : SFin (S k)) ->
  (ts : Vect n (Term sig k)) ->
  IsJust (checkAll x (map (pure (thin x) <$>) ts))

checkThin x (Var y) =
  mapIsJust Var' $
  thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
checkThin x (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)

checkAllThin x [] = ItIsJust
checkAllThin x (t :: ts) =
  appIsJust
    (appIsJust ItIsJust (checkThin x t))
    (checkAllThin x ts)

export
checkJust :
  (x : SFin k) ->
  (t : Term sig k) ->
  (0 _ : check x t = Just u) ->
  t = pure (thin x) <$> u
checkAllJust :
  (x : SFin k) ->
  (ts : Vect n (Term sig k)) ->
  (0 _ : checkAll x ts = Just us) ->
  ts = map (pure (thin x) <$>) us

checkJust x (Var y) prf =
  let 0 z = mapJustInverse Var' (thick x y) prf in
  let 0 prf = thickJust x y (fst z.snd) in
  sym $ Calc $
    |~ pure (thin x) <$> u
    ~~ pure (thin x) <$> Var' z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
    ~~ Var' y                       ...(cong Var' prf)
checkJust x (Op op ts) prf =
  let 0 z = mapJustInverse (Op op) (checkAll x ts) prf in
  let 0 prf = checkAllJust x ts (fst z.snd) in
  Calc $
    |~ Op op ts
    ~~ pure (thin x) <$> Op op z.fst ...(cong (Op op) prf)
    ~~ pure (thin x) <$> u           ...(sym $ cong (pure (thin x) <$>) $ snd z.snd)

checkAllJust x [] Refl = Refl
checkAllJust x (t :: ts) prf =
  let 0 z = appJustInverse (Just (::) <*> check x t) (checkAll x ts) prf in
  let 0 w = appJustInverse (Just (::)) (check x t) (fst z.snd.snd) in
  Calc $
    |~ t :: ts
    ~~ map (pure (thin x) <$>) (w.snd.fst :: z.snd.fst)    ...(cong2 (::) (checkJust x t (fst $ snd w.snd.snd)) (checkAllJust x ts (fst $ snd z.snd.snd)))
    ~~ map (pure (thin x) <$>) (w.fst w.snd.fst z.snd.fst) ...(cong (\f => map (pure (thin x) <$>) (f w.snd.fst z.snd.fst)) $ injective $ fst w.snd.snd)
    ~~ map (pure (thin x) <$>) (z.fst z.snd.fst)           ...(sym $ cong (\f => map (pure (thin x) <$>) (f z.snd.fst)) $ snd $ snd w.snd.snd)
    ~~ map (pure (thin x) <$>) us                          ...(sym $ cong (map (pure (thin x) <$>)) $ snd $ snd z.snd.snd)

-- Single Variable Substitution ------------------------------------------------

export
for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k)
(t `for` x) y = maybe t Var' (thick x y)

export
forRefl :
  (0 u : Term sig (pred k)) ->
  (x : SFin k) ->
  (u `for` x) x = u
forRefl u x = cong (maybe u Var') $ extractIsNothing $ thickRefl x

export
forThin :
  (0 t : Term sig (pred k)) ->
  (x : SFin k) ->
  (t `for` x) . thin x .=. Var'
forThin t x i = cong (maybe t Var') (thickThin x i)

export
forUnifies :
  (x : SFin k) ->
  (t : Term sig k) ->
  (0 _ : check x t = Just u) ->
  (u `for` x) <$> t = (u `for` x) <$> Var' x
forUnifies x t prf = Calc $
  |~ (u `for` x) <$> t
  ~~ (u `for` x) <$> pure (thin x) <$> u ...(cong ((u `for` x) <$>) $ checkJust x t prf)
  ~~ (u `for` x) . thin x <$> u          ...(sym $ subAssoc (u `for` x) (pure (thin x)) u)
  ~~ Var' <$> u                          ...(subCong (forThin u x) u)
  ~~ u                                   ...(subUnit u)
  ~~ (u `for` x) <$> Var' x              ...(sym $ forRefl u x)

-- Substitution List -----------------------------------------------------------

public export
data AList : Signature -> Nat -> Nat -> Type where
  Lin : AList sig n n
  (:<) : AList sig k n -> (Term sig k, SFin (S k)) -> AList sig (S k) n

%name AList sub

namespace Exists
  public export
  (:<) : Exists (AList sig n) -> (Term sig n, SFin (S n)) -> Exists (AList sig (S n))
  Evidence _ sub :< tx = Evidence _ (sub :< tx)

export
eval : AList sig k n -> SFin k -> Term sig n
eval [<] = Var'
eval (sub :< (t, x)) = eval sub . (t `for` x)

export
(++) : AList sig k n -> AList sig j k -> AList sig j n
sub ++ [<] = sub
sub ++ sub1 :< tx = (sub ++ sub1) :< tx

-- Properties

export
recover : Singleton k -> AList sig k n -> Singleton n
recover x [<] = x
recover x (sub :< _) = recover (pure pred <*> x) sub

export
evalHomo :
  (0 sub2 : AList sig k n) ->
  (sub1 : AList sig j k) ->
  eval (sub2 ++ sub1) .=. eval sub2 . eval sub1
evalHomo sub2 [<] i = Refl
evalHomo sub2 (sub1 :< (t, x)) i = Calc $
  |~ eval (sub2 ++ sub1) <$> (t `for` x) i
  ~~ (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)]
  Nothing => Evidence _ [<]

flexRigid : SFin (S n) -> Term sig (S n) -> Maybe (Exists (AList sig (S n)))
flexRigid x t = case check x t of
  Just u => Just (Evidence _ [<(u, x)])
  Nothing => Nothing

export
amgu :
  DecOp sig =>
  (t, u : Term sig n) ->
  Exists (AList sig n) ->
  Maybe (Exists (AList sig n))
amguAll :
  DecOp sig =>
  (ts, us : Vect k (Term sig n)) ->
  Exists (AList sig n) ->
  Maybe (Exists (AList sig n))

amgu (Op op ts) (Op op' us) acc with (decOp (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)
amgu t@(Var _) u@(Var _) (Evidence _ (sub :< (v, z))) =
  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
amgu t@(Var _) u@(Op _ _) (Evidence _ (sub :< (v, z))) =
  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
amgu t@(Op _ _) u@(Var _) (Evidence _ (sub :< (v, z))) =
  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)

amguAll [] [] acc = Just acc
amguAll (t :: ts) (u :: us) acc = do
  acc <- amgu t u acc
  amguAll ts us acc

export
mgu : DecOp sig => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
mgu t u = amgu t u (Evidence _ [<])

-- Properties

export
trivialUnify :
  (0 f : SFin n -> Term sig k) ->
  (t : Term sig n) ->
  (Max (Extension (Unifies t t) f)).Prop Var'
trivialUnify f t = (Refl , \g, prf => varMax g)

export
varElim :
  (x : SFin (S n)) ->
  (t : Term sig (S n)) ->
  (0 _ : check x t = Just u) ->
  (Max (Unifies (Var x) t)).Prop (u `for` x)
varElim x t prf =
  ( sym $ forUnifies x t prf
  , \g, prf' => MkLte (g . thin x) (\i =>
    case decEq x i of
      Yes Refl =>
       Calc $
        |~ g x
        ~~ g <$> t                        ...(prf')
        ~~ g <$> pure (thin x) <$> u      ...(cong (g <$>) $ checkJust i t prf)
        ~~ (g . thin x) <$> u             ...(sym $ subAssoc g (pure (thin x)) u)
        ~~ (g . thin x) <$> (u `for` x) x ..<(cong ((g . thin x) <$>) $ forRefl u x)
      No neq =>
        let isJust = thickNeq x i neq in
        let (y ** thickIsJustY) = extractIsJust isJust in
        let thinXYIsI = thickJust x i thickIsJustY in
        Calc $
          |~ g i
          ~~ g (thin x y)                            ..<(cong g thinXYIsI)
          ~~ (g . thin x) <$> Var' y                 ...(Refl)
          ~~ (g . thin x) <$> (u `for` x) (thin x y) ..<(cong ((g . thin x) <$>) $ forThin u x y)
          ~~ (g . thin x) <$> (u `for` x) i          ...(cong (((g . thin x) <$>) . (u `for` x)) $ thinXYIsI))
  )

flexFlexUnifies :
  (x, y : SFin (S n)) ->
  (Max {sig} (Unifies (Var x) (Var y))).Prop (eval (flexFlex x y).snd)
flexFlexUnifies x y with (thick x y) proof prf
  _ | Just z =
    (Max (Unifies (Var x) (Var y))).cong
      (\i => sym $ subUnit ((Var' z `for` x) i))
      (varElim x (Var y) (cong (map Var') prf))
  _ | Nothing =
    rewrite thickNothing x y (rewrite prf in ItIsNothing) in
    trivialUnify Var' (Var y)

flexRigidUnifies :
  (x : SFin (S n)) ->
  (t : Term sig (S n)) ->
  (0 _ : flexRigid x t = Just sub) ->
  (Max (Unifies (Var x) t)).Prop (eval sub.snd)
flexRigidUnifies x t ok with (check x t) proof prf
  flexRigidUnifies x t Refl | Just u =
    (Max (Unifies (Var x) t)).cong
      (\i => sym $ subUnit ((u `for` x) i))
      (varElim x t prf)

flexRigidFails :
  (x : SFin (S k)) ->
  (op : sig.Operator j) ->
  (ts : Vect j (Term sig (S k))) ->
  (0 _ : IsNothing (flexRigid x (Op op ts))) ->
  Nothing (Unifies (Var x) (Op op ts))
flexRigidFails x op ts isNothing f prf' with (check x (Op op ts)) proof prf
  _ | Nothing =
    let
      (zip ** occurs) = checkNothing x (Op op ts) (rewrite prf in ItIsNothing)
      cycle : (f x = (f <$> zip) + f x)
      cycle = Calc $
        |~ f x
        ~~ f <$> Op op ts    ...(prf')
        ~~ f <$> zip + Var x ...(cong (f <$>) occurs)
        ~~ (f <$> zip) + f x ...(actionHomo f zip (Var x))
      zipIsTop : (zip = Top)
      zipIsTop = invertActionTop zip $ noCycles (f <$> zip) (f x) (sym cycle)
      opIsVar : (Op op ts = Var x)
      opIsVar = trans occurs (cong (+ Var x) zipIsTop)
    in
    absurd opIsVar

stepEquiv :
  (t, u : Term sig (S k)) ->
  (sub : AList sig k j) ->
  (v : Term sig k) ->
  (x : SFin (S k)) ->
  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 _ : DecOp sig}
  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 : DecOp sig => (t, u : Term sig n) -> (sub : Exists (AList sig n)) -> AmguProof t u sub
export
amguAllProof :
  DecOp sig =>
  (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 (decOp (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 _ : DecOp sig}
  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 : DecOp sig => (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