{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}



module T13135 where


import Data.Kind (Type)


class sub :<: sup
  where
    -- | Injection from @sub@ to @sup@
    inj ::  sub sig -> sup sig

instance (sub :<: sup) => (sub :<: AST sup)
  where
    inj = Sym . inj


data Sig a = Full a | (:->) a (Sig a)

infixr :->

type Sym t = (Sig t -> Type)

data AST :: Sym t -> Sym t
  where
    Sym  :: sym sig -> AST sym sig
    (:$) :: AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig

-- | Generic N-ary syntactic construct
--
-- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic
-- function.
data Constr sig = Constr String

smartSym :: (sub :<: sup) => sub sig -> SmartFun sup sig
smartSym = error "urk"

type family   SmartFun (sym :: Sig t -> Type) sig = f | f -> sym sig  where
-- In full glory:
-- type family SmartFun {t} (sym :: Sig t -> Type) (sig :: Sig t) :: *
--            = f | f -> {t} sym sig  where
  SmartFun sym (Full a)    = AST sym (Full a)
  SmartFun sym (a :-> sig) = AST sym (Full a) -> SmartFun sym sig

-- | Get the length of an array
arrLen ::  AST Constr (Full [a]) -> AST Constr (Full Int)
arrLen = smartSym sym where
  sym = Constr "arrLen"



{- The original bug was a failure to substitute
   properly during type-function improvement.

--------------------------------------
doTopReact
  [WD] hole{a1y1} {0}:: (SmartFun
                           t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2] :: *)
                        GHC.Prim.~#
                        (s_a1y0[fuv:0] :: *) (CFunEqCan)
matchFamTcM
  Matching: SmartFun t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2]
  Match failed
improveTopFunEqs
  SmartFun [t_a1x9[tau:2], sup_a1xb[tau:2],
            sig_a1xc[tau:2]] s_a1y0[fuv:0]
  [* ~ t_a1x9[tau:2], Constr (Sig *) ~ sup_a1xb[tau:2],
   (':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] ~ sig_a1xc[tau:2]]

Emitting new derived equality
  [D] _ {0}:: (* :: *) GHC.Prim.~# (t_a1x9[tau:2] :: *)
  [D] _ {0}:: (Constr (Sig *) :: (Sig * -> *))
                GHC.Prim.~#
              (sup_a1xb[tau:2] :: (Sig t_a1x9[tau:2] -> *))
  [D] _ {0}:: ((':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] :: Sig *)
              GHC.Prim.~#
              (sig_a1xc[tau:2] :: Sig t_a1x9[tau:2])

but sig_a1y3 :: Sig t   BAD
--------------------------------------

Instance
  forall t (sig :: Sig t) (a :: t) (sym :: Sig t -> *).
    SmartFun t sym ((:->) t a sig) = AST t sym (Full t a) -> SmartFun t sym sig

Wanted:
  SmartFun t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2] ~ s_a1y0[fuv:0]
  s_a1y0[fuv:0]  ~  AST * (Constr (Sig *))
                          ('Full * [a_a1wT[sk:2]])
                    -> AST * (Constr (Sig *)) ('Full * Int)

Substitution after matching RHSs
  [ t -> *
  , (sym :: Sig t -> *) -> Constr (Sig *)
  , a -> a_a1wT ]

add sig -> sig0 :: Sig t   -- Or rather Sig *

Apply to LHS

   SmartFun * (Constr (Sig *)) ((:->) * a_a1wT sig0)


improveTopFunEqs
  SmartFun [t_a1x9[tau:2], sup_a1xb[tau:2],
            sig_a1xc[tau:2]] s_a1y0[fuv:0]
  [* ~ t_a1x9[tau:2], Constr (Sig *) ~ sup_a1xb[tau:2],
   (':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] ~ sig_a1xc[tau:2]]
-}