{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module T12444 where

data Nat = Zero | Succ Nat

data SNat (n :: Nat) where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
  m :+: Zero = m
  m :+: (Succ n) = Succ (m :+: n)

foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b))
foo _ x = x


{-
sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m)
     => SNat m -> SNat n -> SNat (m :+: n)
sadd SZero n = n
-}

{- [G]  a ~ Succ c
        Succ c + b ~ Succ (c+b)
        a ~ Zero

-->
        Zero ~ Succ c            TyEq
        fsk1 ~ Succ fsk2         TyEq
        fsk1 ~ (Succ c) + b      FunEq
        fsk2 ~ c+b               FunEq
----
[W] b ~ a+b  --->   b ~ Succ (c+b)


Derived
       a ~ Succ c
       fsk1 ~ Succ fsk2
       b ~ Succ fsk2

work   (Succ c) + b ~ fsk1
       c+b ~ fsk2


-}

{-

[G] a ~ [b]
--> Derived shadow [D] a ~ [b]
    When adding this to the model
    don't kick out a derived shadow again!

[G] (a ~ b)  --> sc   a ~~ b, a ~# b
  Silly to then kick out (a~b) and (a~~b)
  and rewrite them to (a~a) and (a~~a)

Insoluble constraint does not halt solving;
indeed derived version stays. somehow
-}