content: {-# LANGUAGE Haskell2010 #-}
  {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
  {-# LANGUAGE UnicodeSyntax #-}
  {-# LANGUAGE EmptyDataDecls #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  
  module T5329 where
  
  data PZero
  data PSucc p
  
  data Peano n where
    PZero ∷ Peano PZero
    PSucc ∷ IsPeano p ⇒ Peano p → Peano (PSucc p)
  
  class IsPeano n where
    peano ∷ Peano n
  
  instance IsPeano PZero where
    peano = PZero
  
  instance IsPeano p ⇒ IsPeano (PSucc p) where
    peano = PSucc peano 
  
  class (n ~ PSucc (PPred n)) ⇒ PHasPred n where
    type PPred n
  
  instance PHasPred (PSucc p) where
    type PPred (PSucc p) = p
  
  pPred ∷ Peano (PSucc p) → Peano p
  pPred (PSucc p) = p
  
  infixl 6 :+:
  
  class (IsPeano n, IsPeano m, IsPeano (n :+: m), (n :+: m) ~ (m :+: n))
        ⇒ PAdd n m where
    type n :+: m
  
  instance PAdd PZero PZero where
    type PZero :+: PZero = PZero
  
  instance IsPeano p ⇒ PAdd PZero (PSucc p) where
    type PZero :+: (PSucc p) = PSucc p
  
  instance IsPeano p ⇒ PAdd (PSucc p) PZero where
    type (PSucc p) :+: PZero = PSucc p
  
  instance (IsPeano n, IsPeano m, PAdd n m) ⇒ PAdd (PSucc n) (PSucc m) where
    type (PSucc n) :+: (PSucc m) = PSucc (PSucc (n :+: m))
  
  data PAddResult n m r where
    PAddResult ∷ (PAdd n m, PAdd m n, (n :+: m) ~ r)
               ⇒ PAddResult n m r
  
  pAddLeftZero ∷ ∀ n . IsPeano n ⇒ PAddResult PZero n n
  pAddLeftZero = case peano ∷ Peano n of
    PZero   → PAddResult
    PSucc _ → PAddResult
  
  pAddRightZero ∷ ∀ n . IsPeano n ⇒ PAddResult n PZero n
  pAddRightZero = case peano ∷ Peano n of
    PZero   → PAddResult
    PSucc _ → PAddResult
  
  data PAddSucc n m where
    PAddSucc ∷ (PAdd n m, PAdd m n,
                PAdd (PSucc n) m, PAdd m (PSucc n),
                PAdd n (PSucc m), PAdd (PSucc m) n,
                (PSucc n :+: m) ~ PSucc (n :+: m),
                (n :+: PSucc m) ~ PSucc (n :+: m))
             ⇒ PAddSucc n m
  
  pAddSucc ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAddSucc n m
  pAddSucc = case (peano ∷ Peano n, peano ∷ Peano m) of
    (PZero,   PZero)   → PAddSucc
    (PZero,   PSucc _) → case pAddLeftZero ∷ PAddResult n (PPred m) (PPred m) of
      PAddResult → PAddSucc
    (PSucc _, PZero)   → case pAddRightZero ∷ PAddResult (PPred n) m (PPred n) of
      PAddResult → PAddSucc
    (PSucc _, PSucc _) → case pAddSucc ∷ PAddSucc (PPred n) (PPred m) of
      PAddSucc → PAddSucc
  
  data PAdd2 n m where
    PAdd2 ∷ (PAdd n m, PAdd m n) ⇒ PAdd2 n m
  
  pAdd2 ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAdd2 n m
  pAdd2 = case (peano ∷ Peano n, peano ∷ Peano m) of
    (PZero,   PZero)   → PAdd2
    (PZero,   PSucc _) → PAdd2
    (PSucc _, PZero)   → PAdd2
    (PSucc _, PSucc _) → case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
      PAdd2 → PAdd2
  
  data PAdd3 n m k where
    PAdd3 ∷ (PAdd n m, PAdd m k, PAdd m n, PAdd k m, PAdd n k, PAdd k n,
             PAdd (n :+: m) k, PAdd k (m :+: n),
             PAdd n (m :+: k), PAdd (m :+: k) n,
             PAdd (n :+: k) m, PAdd m (n :+: k),
             ((n :+: m) :+: k) ~ (n :+: (m :+: k)),
             (m :+: (n :+: k)) ~ ((m :+: n) :+: k))
          ⇒ PAdd3 n m k
  
  pAdd3 ∷ ∀ n m k . (IsPeano n, IsPeano m, IsPeano k) ⇒ PAdd3 n m k
  pAdd3 = case (peano ∷ Peano n, peano ∷ Peano m, peano ∷ Peano k) of
    (PZero,   PZero,   PZero)   → PAdd3
    (PZero,   PZero,   PSucc _) → PAdd3
    (PZero,   PSucc _, PZero)   → PAdd3
    (PSucc _, PZero,   PZero)   → PAdd3
    (PZero,   PSucc _, PSucc _) →
      case pAdd2 ∷ PAdd2 (PPred m) (PPred k) of
        PAdd2 → PAdd3
    (PSucc _, PZero,   PSucc _) →
      case pAdd2 ∷ PAdd2 (PPred n) (PPred k) of
        PAdd2 → PAdd3
    (PSucc _, PSucc _, PZero)   →
      case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
        PAdd2 → PAdd3
    (PSucc _, PSucc _, PSucc _) → 
      case pAdd3 ∷ PAdd3 (PPred n) (PPred m) (PPred k) of
        PAdd3 → case pAddSucc ∷ PAddSucc (PPred n :+: PPred m) (PPred k) of
          PAddSucc → case pAddSucc ∷ PAddSucc (PPred n :+: PPred k) (PPred m) of
            PAddSucc → case pAddSucc ∷ PAddSucc (PPred m :+: PPred k) (PPred n) of 
              PAddSucc → PAdd3
  
  