{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
module Language.Symantic.Typing.Type
 ( module Language.Symantic.Typing.Type
 , Proxy(..)
 , (:~:)(..)
 , (:~~:)(..)
 , K.Constraint
 ) where

import Control.Applicative (Alternative(..))
import Data.Maybe (isJust)
import Data.Proxy
import Data.Semigroup ((<>))
import Data.Set (Set)
import Data.Type.Equality
import Data.Typeable
import qualified Data.Kind as K
import qualified Data.Set as Set

import Language.Symantic.Grammar
import Language.Symantic.Typing.List
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.Module

-- * Type 'Type'
data Type (src::K.Type) (vs::[K.Type]) (t::kt) where
	TyConst :: src -> Len vs
	               -> Const src c
	               -> Type src vs c
	TyApp   :: src -> Type src vs f
	               -> Type src vs a
	               -> Type src vs (f a)
	               -- NOTE: @f a@ decomposition made possible
	               -- at the cost of requiring @TypeInType@.
	TyVar   :: src -> NameVar
	               -> Var src vs v
	               -> Type src vs v
	TyFam   :: src -> Len vs
	               -> Const src fam
	               -> Types src vs hs
	               -> Type src vs (Fam fam hs)
	{-
	TyPi    :: src -> Type src (arg ': vs) res
	               -> Type (Pi arg res) src vs
	TyQuant :: src -> NameHint
	               -> Kind src kv
	               -> (forall (v::kv). Type src vs v -> TypeK src vs k)
	               -> Type src vs (h::k)
	TyEq :: src -> Type x src vs
	            -> Type y src vs
	            -> Type (x #~ y) src vs
	-}

pattern a :$ b <- TyApp _ a b
infixr 0 :$
pattern a :@ b <- TyApp _ a b
infixl 9 :@

instance Source src => Eq (Type src vs t) where
	x == y = isJust $ eqType x y
instance SourceInj (TypeVT src) src => TestEquality (Type src vs) where
	testEquality = eqType

type instance SourceOf (Type src vs t) = src
instance Source src => Sourceable (Type src vs t) where
	sourceOf (TyConst src _l _c)     = src
	sourceOf (TyApp   src _f _a)     = src
	sourceOf (TyVar   src _n _v)     = src
	sourceOf (TyFam   src _l _f _as) = src
	
	setSource (TyConst _src l c)    src = TyConst src l c
	setSource (TyApp   _src f a)    src = TyApp   src f a
	setSource (TyVar   _src n v)    src = TyVar   src n v
	setSource (TyFam   _src l f as) src = TyFam   src l f as

instance SourceInj (TypeVT src) src => KindOf (Type src vs) where
	kindOf t = kindOfType t `withSource` TypeVT t

instance ConstsOf (Type src vs t) where
	constsOf (TyConst _src _len c)    = Set.singleton $ ConstC c
	constsOf TyVar{}                  = Set.empty
	constsOf (TyApp _src f a)         = constsOf f `Set.union` constsOf a
	constsOf (TyFam _src _len fam as) = constsOf fam `Set.union` constsOf as

type instance VarsOf (Type src vs t) = vs
instance LenVars (Type src vs t) where
	lenVars (TyConst _src len _c) = len
	lenVars (TyApp _src f _a)     = lenVars f
	lenVars (TyVar   _src _n v)   = lenVars v
	lenVars (TyFam _src l _f _as) = l
instance UsedVarsOf (Type src vs t) where
	usedVarsOf vs TyConst{} k = k vs
	usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
	usedVarsOf vs (TyApp _src f a) k =
		usedVarsOf vs f $ \vs' ->
		usedVarsOf vs' a k
	usedVarsOf vs (TyVar _src _n v) k =
		case insertUsedVars v vs of
		 Nothing  -> k vs
		 Just vs' -> k vs'
instance VarOccursIn (Type src vs t) where
	varOccursIn v (TyVar _src _n v') | Just{} <- v `eqVarKi` v' = False
	varOccursIn _v TyVar{}                  = False
	varOccursIn _v TyConst{}                = False
	varOccursIn v (TyApp _src f a)          = varOccursIn v f || varOccursIn v a
	varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
instance AllocVars (Type src) where
	allocVarsL len (TyConst src l c)  = TyConst src (addLen len l) c
	allocVarsL len (TyApp src f a)    = TyApp src (allocVarsL len f) (allocVarsL len a)
	allocVarsL len (TyVar src n v)    = TyVar src n $ allocVarsL len v
	allocVarsL len (TyFam src l f as) = TyFam src (addLen len l) f $ allocVarsL len `mapTys` as
	
	allocVarsR len (TyConst src l c)  = TyConst src (addLen l len) c
	allocVarsR len (TyApp src f a)    = TyApp src (allocVarsR len f) (allocVarsR len a)
	allocVarsR len (TyVar src n v)    = TyVar src n $ allocVarsR len v
	allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as

-- | Like 'TyConst', but using 'noSource', 'lenInj' and 'constInj'.
-- 
-- FIXME: remove @kc@ when GHC's #12933 is fixed.
tyConst ::
 forall kc (c::kc) src vs.
 Source src =>
 LenInj vs =>
 Constable c =>
 KindInjP (Ty_of_Type kc) =>
 Type_of_Ty (Ty_of_Type kc) ~ kc =>
 Type src vs c
tyConst = TyConst noSource lenInj constInj
 -- NOTE: The forall brings @c@ first in the type variables,
 -- which is convenient to use @TypeApplications@.

-- | Like 'tyConst', but not using 'lenInj'.
tyConstLen ::
 forall kc (c::kc) src vs.
 Source src =>
 Constable c =>
 KindInjP (Ty_of_Type kc) =>
 Type_of_Ty (Ty_of_Type kc) ~ kc =>
 Len vs ->
 Type src vs c
tyConstLen len = TyConst noSource len constInj

-- | Like 'TyApp', but using 'noSource'.
tyApp ::
 Source src =>
 Type src vs f ->
 Type src vs a ->
 Type src vs (f a)
tyApp = TyApp noSource
infixl 9 `tyApp`

-- | Like 'TyVar', but using 'noSource'.
tyVar ::
 Source src =>
 NameVar ->
 Var src vs v ->
 Type src vs v
tyVar = TyVar noSource

-- | Like 'TyFam', but using 'noSource'.
-- 
-- FIXME: remove @kc@ when GHC's #12933 is fixed.
tyFam ::
 forall kc (c::kc) as vs src.
 Source src =>
 LenInj vs =>
 Constable c =>
 KindInjP (Ty_of_Type kc) =>
 Type_of_Ty (Ty_of_Type kc) ~ kc =>
 Types src vs as ->
 Type src vs (Fam c as)
tyFam = TyFam noSource lenInj (constInj @c)

-- | Qualify a 'Type'.
tyQual ::
 Source src =>
 Type src vs q ->
 Type src vs t ->
 (Qual q ->
  Type src vs t ->
  Type src vs (q #> t)) ->
 Type src vs (q #> t)
tyQual q t f =
	case proveConstraint q of
	 Just Dict -> f Dict t
	 Nothing -> q #> t
infix 1 `tyQual`

-- ** Type 'TypeK'
-- | Existential 'Type' of a known 'Kind'.
data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t)
type instance SourceOf (TypeK src vs ki) = src
type instance VarsOf (TypeK src vs ki) = vs
instance Source src => Eq (TypeK src vs ki) where
	TypeK x == TypeK y = isJust $ eqType x y

-- ** Type 'TypeT'
-- | Existential for 'Type'.
data TypeT src vs = forall t. TypeT (Type src vs t)
type instance SourceOf (TypeT src vs) = src
type instance VarsOf (TypeT src vs) = vs
instance Source src => Eq (TypeT src vs) where
	TypeT x == TypeT y = isJust $ eqTypeKi x y

-- ** Type 'TypeVT'
-- | Existential polymorphic 'Type'.
data TypeVT src = forall vs t. TypeVT (Type src vs t)
type instance SourceOf (TypeVT src) = src
instance Source src => Eq (TypeVT src) where
	TypeVT x == TypeVT y =
		let (x', y') = appendVars x y in
		isJust $ eqTypeKi x' y'

-- * Type 'Const'
-- | /Type constant/.
data Const src (c::kc) where
	Const :: Constable c => Kind src kc -> Const src (c::kc)

type instance SourceOf (Const src c) = src
instance ConstsOf (Const src c) where
	constsOf = Set.singleton . ConstC
instance SourceInj (ConstC src) src => KindOf (Const src) where
	kindOf c@(Const kc) = kc `withSource` ConstC c

kindOfConst :: Const src (t::kt) -> Kind src kt
kindOfConst (Const kc) = kc

-- ** Class 'Constable'
class
 ( Typeable c
 , FixityOf c
 , NameTyOf c
 , ClassInstancesFor c
 , TypeInstancesFor c
 ) => Constable c
instance
 ( Typeable c
 , FixityOf c
 , NameTyOf c
 , ClassInstancesFor c
 , TypeInstancesFor c
 ) => Constable c

-- ** Class 'ConstsOf'
-- | Return the 'Const's used by something.
class ConstsOf a where
	constsOf :: a -> Set (ConstC (SourceOf a))

-- ** Type 'ConstC'
data ConstC src
 = forall c. ConstC (Const src c)
instance Eq (ConstC src) where
 ConstC x == ConstC y = isJust $ x `eqConstKi` y
instance Ord (ConstC src) where
 ConstC x `compare` ConstC y = x `ordConst` y

-- * Type '(->)'
-- | The function 'Type' @(->)@,
-- with an infix notation more readable.
(~>) ::
 Source src =>
 Constable (->) =>
 Type src vs a ->
 Type src vs b ->
 Type src vs (a -> b)
(~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b
infixr 0 ~>
instance FixityOf (->) where
	fixityOf _c = Just $ Fixity2 $ infixR 0
{- NOTE: defined in Lib.Function
instance ClassInstancesFor (->)
instance TypeInstancesFor  (->)
-}

-- ** Type family 'FunArg'
type family FunArg (fun::K.Type) :: K.Type where
	FunArg (q #> f) = FunArg f
	FunArg (a -> b) = a

-- ** Type family 'FunRes'
type family FunRes (fun::K.Type) :: K.Type where
	FunRes (q #> f) = FunRes f
	FunRes (a -> b) = b

-- | Return, when the given 'Type' is a function,
-- the argument of that function.
unTyFun ::
 forall t src tys.
 SourceInj (TypeVT src) src =>
 Constable (->) =>
 Type src tys t ->
 Maybe ( Type src tys (FunArg t)
       , Type src tys (FunRes t) )
unTyFun ty_ini = go ty_ini
	where
	go ::
	 Type src tys x ->
	 Maybe ( Type src tys (FunArg x)
	       , Type src tys (FunRes x) )
	go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
	 | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
	 = Just ((a `withSource` TypeVT ty_ini), (b `withSource` TypeVT ty_ini))
	go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
	 = go b
	go TyApp{}   = Nothing
	go TyConst{} = Nothing
	go TyVar{}   = Nothing
	go TyFam{}   = Nothing

-- ** Type @(#>)@
-- | /Type constant/ to qualify a 'Type'.
newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)
instance NameTyOf (#>) where
	nameTyOf _c = [] `Mod` "=>"
instance FixityOf (#>) where
	fixityOf _c = Just $ Fixity2 $ infixR 0
instance ClassInstancesFor (#>)
instance TypeInstancesFor  (#>)

-- | Qualify a 'Type'.
(#>) ::
 Source src =>
 Type src vs q ->
 Type src vs t ->
 Type src vs (q #> t)
(#>) q t = (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
infixr 0 #>
 -- NOTE: should actually be (-1)
 -- to compose well with @infixr 0 (->)@
 -- but this is not allowed by GHC.

-- ** Class @(#)@
-- | 'K.Constraint' union.
class    (x, y) => x # y
instance (x, y) => x # y
instance NameTyOf (#) where
	nameTyOf _c = [] `Mod` ","
instance FixityOf (#) where
	fixityOf _c = Just $ Fixity2 $ infixB SideL 0
instance ClassInstancesFor (#) where
	proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1)
	 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c
	 , Just Dict <- proveConstraint q0
	 , Just Dict <- proveConstraint q1
	 = Just Dict
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor (#)

-- | Unify two 'K.Constraint's.
(#) ::
 Source src =>
 Type src vs qx ->
 Type src vs qy ->
 Type src vs (qx # qy)
(#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
infixr 2 #

-- ** Type @(() :: @'K.Constraint'@)@
instance NameTyOf (()::K.Constraint) where
	nameTyOf _c = [] `Mod` "()"
-- instance FixityOf (()::Constraint)
instance ClassInstancesFor (()::K.Constraint) where
	proveConstraintFor _c q
	 | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q
	 = Just Dict
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor (()::K.Constraint)

-- | Like 'noConstraintLen', but using 'lenInj'.
noConstraint :: Source src => LenInj vs => Type src vs (()::K.Constraint)
noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) lenInj

-- | Empty 'K.Constraint'.
noConstraintLen :: Source src => Len vs -> Type src vs (()::K.Constraint)
noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)

-- ** Class @(#~)@
-- | /Type equality/ 'K.Constraint'.
class    (x ~ y) => x #~ y
instance (x ~ y) => x #~ y
instance NameTyOf (#~) where
	nameTyOf _c = [] `Mod` "~"
	isNameTyOp _c = True
instance FixityOf (#~) where
	fixityOf _ = Just $ Fixity2 $ infixB SideL 0
instance
 ( KindInj k
 , Typeable k
 ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where
	proveConstraintFor _c (TyApp _ (TyApp _ c a) b)
	 | Just HRefl <- proj_ConstKiTy @(k -> k -> K.Constraint) @(#~) c
	 , Just Refl  <- eqType a b
	 = Just Dict
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor  (#~)

-- | Constraint two 'Type's to be equal.
(#~) ::
 forall k a b src vs.
 Source src =>
 Typeable k =>
 KindInj k =>
 Type src vs (a :: k) ->
 Type src vs (b :: k) ->
 Type src vs (a #~ b)
(#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b
infixr 2 #~

-- | /Type equality/.
eqType ::
 Source src =>
 Type src tys (x::k) ->
 Type src tys (y::k) ->
 Maybe (x:~:y)
eqType x y | Just HRefl <- eqTypeKi x y = Just Refl
eqType _x _y = Nothing

-- | /Heterogeneous type equality/:
-- return two proofs when two 'Type's are equals:
-- one for the type and one for the kind.
eqTypeKi ::
 Source src =>
 Type src tys (x::kx) ->
 Type src tys (y::ky) ->
 Maybe (x:~~:y)
eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y
eqTypeKi (TyVar   _sx _nx x) (TyVar   _sy _ny y) = eqVarKi   x y
eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay)
 | Just HRefl <- eqTypeKi fx fy
 , Just HRefl <- eqTypeKi ax ay
 = Just HRefl
eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
 | Just HRefl <- eqConstKi fx fy
 , Just HRefl <- eqTypes ax ay
 = Just HRefl
-- NOTE: 'TyFam' is expanded as much as possible.
eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y
eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y)
eqTypeKi _x _y = Nothing

eqTypes ::
 Source src =>
 Types src tys x ->
 Types src tys y ->
 Maybe (x:~~:y)
eqTypes TypesZ TypesZ = Just HRefl
eqTypes (x `TypesS` sx) (y `TypesS` sy)
 | Just HRefl <- eqTypeKi x y
 , Just HRefl <- eqTypes sx sy
 = Just HRefl
eqTypes _x _y = Nothing

-- *** Comparison
-- | Compare two 'Type's.
ordType ::
 Source src =>
 Type src tys (x::kx) ->
 Type src tys (y::ky) ->
 Ordering
-- NOTE: 'TyFam' is expanded as much as possible.
ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay
ordType x@TyFam{} y = ordType (expandFam x) y
ordType x y@TyFam{} = ordType x (expandFam y)
ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y
ordType TyConst{} _y = LT
ordType _x TyConst{} = GT
ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y
ordType TyVar{} _y = LT
ordType _x TyVar{} = GT
ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy
-- ordType TyApp{} _y = LT
-- ordType _x TyApp{} = GT

ordTypes ::
 Source src =>
 Types src tys x ->
 Types src tys y ->
 Ordering
ordTypes TypesZ TypesZ   = EQ
ordTypes TypesZ TypesS{} = LT
ordTypes TypesS{} TypesZ = GT
ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy

-- * Type 'Qual'
-- | Captures the proof of a 'K.Constraint'
-- (and its dictionaries when it contains type classes):
-- pattern matching on the 'Dict' constructor
-- brings the 'K.Constraint' into scope.
data Qual q where
	Dict :: q => Qual q

-- ** Class 'ClassInstancesFor'
class ClassInstancesFor c where
	proveConstraintFor
	 :: Source src
	 => proxy c
	 -> Type src vs q
	 -> Maybe (Qual q)
	proveConstraintFor _c _q = Nothing

proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
proveConstraint q = foldr proj Nothing $ constsOf q
	where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)

-- ** Injection
constInj ::
 forall c src.
 Source src =>
 Constable c =>
 KindInjP (Ty_of_Type (K c)) =>
 Type_of_Ty (Ty_of_Type (K c)) ~ K c =>
 Const src c
constInj = Const $ kindInjP @(Ty_of_Type (K c)) noSource

constKiInj ::
 forall kc c src.
 Source src =>
 Constable c =>
 Kind src kc ->
 Const src (c::kc)
constKiInj = Const

-- ** Projection
{- XXX: not working because of GHC's #12933
proj_ConstKi ::
 forall c u src.
 Constable c =>
 (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>
 KindInj (K c) =>
 Const src u ->
 Maybe (c :~~: u)
proj_ConstKi (Const ku) = do
	Refl <- eqKind ku $ kindInj @(K c) @()
	Refl :: u:~:c <- eqT
	Just HRefl
-}

-- | Like 'proj_ConstKi', but with kind equality already known.
proj_Const ::
 forall c u src.
 Typeable c =>
 Const src u ->
 Maybe (c :~: u)
proj_Const Const{} = eqT

-- | Like 'proj_Const', but on a 'Type'.
proj_ConstTy ::
 forall c u src vs.
 Typeable c =>
 Type src vs u ->
 Maybe (c :~: u)
proj_ConstTy (TyConst _src _len Const{}) = eqT
proj_ConstTy _ = Nothing

-- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely,
-- when used multiple times in the same pattern match,
-- because of GHC's #12933.
proj_ConstKi ::
 forall kc (c::kc) u src.
 Typeable c =>
 (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 KindInjP (Ty_of_Type kc) =>
 Const src u ->
 Maybe (c :~~: u)
proj_ConstKi (Const ku) = do
	Refl <- eqKind ku $ kindInjP @(Ty_of_Type kc) ()
	Refl :: u:~:c <- eqT
	Just HRefl

-- | Like 'proj_ConstKi', but on a 'Type'.
proj_ConstKiTy ::
 forall kc (c::kc) u src vs.
 Typeable c =>
 (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 KindInjP (Ty_of_Type kc) =>
 Type src vs u ->
 Maybe (c :~~: u)
proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c
proj_ConstKiTy _ = Nothing

eqConst ::
 Const src_x (x::k) ->
 Const src_y (y::k) ->
 Maybe (x:~:y)
eqConst (Const _kx) (Const _ky) = eqT
instance Eq (Const src c) where
	x == y = isJust $ eqConstKi x y
instance Ord (Const src c) where
	compare = ordConst

eqConstKi ::
 forall src_x src_y kx ky x y.
 Const src_x (x::kx) ->
 Const src_y (y::ky) ->
 Maybe (x:~~:y)
eqConstKi (Const kx) (Const ky)
 | Just Refl <- eqKind kx ky
 , Just (Refl::x:~:y) <- eqT
 = Just HRefl
eqConstKi _x _y = Nothing

ordConst ::
 forall src_x src_y kx ky x y.
 Const src_x (x::kx) ->
 Const src_y (y::ky) ->
 Ordering
ordConst x@Const{} y@Const{} =
	typeRep x `compare` typeRep y

normalizeQualsTy ::
 Source src =>
 Type src tys (t::kt) ->
 TypeK src tys kt
normalizeQualsTy = go
	where
	go ::
	 Source src =>
	 Type src tys (a::ka) ->
	 TypeK src tys ka
	-- (q0, q1)
	go (TyApp s1 (TyApp s0 f q0) q1)
	 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f
	 , TypeK q0' <- go q0
	 , TypeK q1' <- go q1 =
		case (proveConstraint q0', proveConstraint q1') of
		 (Just{}, Just{})  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0
		 (Just{}, Nothing) -> TypeK q1'
		 (Nothing, Just{}) -> TypeK q0'
		 (Nothing, Nothing) ->
			case q0' `ordType` q1' of
			 LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1'
			 EQ -> TypeK $ q0'
			 GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0'
	-- q0 => (q1 => t)
	go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t))
	 | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0
	 , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1
	 , TypeK q0' <- go q0
	 , TypeK q1' <- go q1 =
		case (proveConstraint q0', proveConstraint q1') of
		 (Just{}, Just{})  -> TypeK t
		 (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t
		 (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t
		 (Nothing, Nothing) ->
			case q0' `ordType` q1' of
			 LT ->
				let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ constInj @(#)) q0') q1' in
				TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t
			 EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t
			 GT ->
				let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ constInj @(#)) q1') q0' in
				TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t
	-- q => t
	go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c =
		case proveConstraint q of
		 Just{} -> go t
		 Nothing
		  | TypeK q' <- go q
		  , TypeK t' <- go t
		  -> TypeK $ q' #> t'
	-- q
	go q
	 | Just Refl <- KiConstraint () `eqKind` kindOfType q
	 = case proveConstraint q of
		 Just{}  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q
		 Nothing -> TypeK q
	go (TyApp src f a)
	 | TypeK f' <- go f
	 , TypeK a' <- go a
	 = TypeK $ TyApp src f' a'
	go t@TyFam{}   = go (expandFam t)
	go t@TyConst{} = TypeK t
	go t@TyVar{}   = TypeK t

-- * Type family 'Fam'
-- | Apply the /type family/ selected by @fam@
-- to a list of types (within a 'Proxy').
-- 
-- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s.
type family Fam (fam::k) (hs::[K.Type]) :: k
-- type family FamKi fam :: K.Type

-- ** Class 'TypeInstancesFor'
class TypeInstancesFor (c::kc) where
	expandFamFor
	 :: Source src
	 => proxy c
	 -> Len vs
	 -> Const src fam
	 -> Types src vs ts
	 -> Maybe (Type src vs (Fam fam ts))
	expandFamFor _c _len _fam _as = Nothing

-- ** Class 'ExpandFam'
class ExpandFam a where
	expandFam :: Source (SourceOf a) => a -> a
instance ExpandFam (Type src vs t) where
	expandFam t@TyConst{} = t
	expandFam t@TyVar{} = t
	expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a)
	expandFam t@(TyFam _src len fam as) =
		case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of
		 Nothing -> t
		 Just t' -> expandFam t'
		where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as)
		-- XXX: this can loop…

-- | Like 'kindOf' but keep the old 'Source'.
kindOfType :: Type src vs (t::kt) -> Kind src kt
kindOfType (TyConst _src _l c) = kindOfConst c
kindOfType (TyApp _src f _a) =
	case kindOfType f of
	 KiFun _src_kf _kx kf -> kf
kindOfType (TyVar _src _n v)         = kindOfVar v
kindOfType (TyFam _src _len fam _as) = kindOfConst fam

-- | Remove unused 'Var's from the context.
normalizeVarsTy ::
 Type src vs (t::kt) ->
 (forall vs'. Type src vs' (t::kt) -> ret) -> ret
normalizeVarsTy ty k =
	usedVarsOf UsedVarsZ ty $ \vs ->
	k $ goTy vs ty
	where
	goTy ::
	 UsedVars src vs vs' ->
	 Type src vs t ->
	 Type src vs' t
	goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c
	goTy vs (TyApp src f a)      = TyApp src (goTy vs f) (goTy vs a)
	goTy vs (TyVar src n v) =
		case v `lookupUsedVars` vs of
		 Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail"
		 Just v' -> TyVar src n v'
	goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as
	
	goTys ::
	 UsedVars src vs vs' ->
	 Types src vs ts ->
	 Types src vs' ts
	goTys _vs TypesZ = TypesZ
	goTys vs (TypesS t ts) =
		goTy vs t `TypesS`
		goTys vs ts

-- * Type 'Types'
data Types src vs (ts::[K.Type]) where
	TypesZ :: Types src vs '[]
	TypesS :: Type src vs t
	       -> Types src vs ts
	       -> Types src vs (Proxy t ': ts)
infixr 5 `TypesS`

type instance SourceOf (Types src vs ts) = src
instance ConstsOf (Types src vs ts) where
	constsOf TypesZ = Set.empty
	constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts
type instance VarsOf (Types src vs ts) = vs
instance UsedVarsOf (Types src vs ts) where
	usedVarsOf vs TypesZ k = k vs
	usedVarsOf vs (TypesS t ts) k =
		usedVarsOf vs t $ \vs' ->
		usedVarsOf vs' ts k
instance VarOccursIn (Types src vs ts) where
	varOccursIn _v TypesZ = False
	varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts

mapTys ::
 (forall kt (t::kt). Type src vs t -> Type src vs' t) ->
 Types src vs  ts ->
 Types src vs' ts
mapTys _f TypesZ = TypesZ
mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts

foldlTys ::
 (forall k (t::k). Type src vs t -> acc -> acc) ->
 Types src vs ts -> acc -> acc
foldlTys _f TypesZ acc = acc
foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)

-- * Class 'TypeOf'
class TypeOf a where
	typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t