1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE PatternSynonyms #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE StandaloneDeriving #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 {-# LANGUAGE UndecidableSuperClasses #-}
8 {-# LANGUAGE ViewPatterns #-}
9 {-# OPTIONS_GHC -Wno-partial-fields #-}
11 module Symantic.Typer.Type where
13 import Control.Monad.Classes as MC ()
14 import Control.Monad.Classes.Run as MC ()
15 import Data.Eq (Eq (..))
16 import Data.Function (($))
17 import Data.Functor ((<$>))
18 import Data.Map.Strict qualified as Map
19 import Data.Maybe (Maybe (..), isJust)
20 import Data.Monoid (Monoid (..))
21 import Data.Proxy (Proxy (..))
22 import Data.Semigroup (Semigroup (..))
23 import Data.String (String)
25 import Text.Show (Show (..))
26 import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..), pattern App)
27 import Prelude qualified
29 import Symantic.Typer.Eq
30 import Symantic.Typer.List
32 data WithProv prov a = WithProv {withProv :: prov, unWithProv :: a}
44 data Var :: forall vK. Prov -> [Type] -> vK -> Type where
46 { varZKind :: Kind prov vK
49 Var prov (Proxy (v :: vK) ': ws) (v :: vK)
50 VarS :: Var prov vs v -> Var prov (not_v ': vs) v
51 deriving instance Show prov => Show (Var prov vs v)
53 pattern Var :: () => () => Kind prov vK -> Len ws -> Var prov vs' (v :: vK)
54 pattern Var{varKind, varNext} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext})
58 data VarVS prov (v :: vK) = forall vs. VarVS (Var prov vs v)
59 var :: Var prov vs (v :: vK) -> VarVS prov (v :: vK)
60 var v@VarZ{} = VarVS v
63 instance EqTy (Var prov vs) (Var prov vs) where
64 eqTy VarZ{} VarZ{} = Just HRefl
65 eqTy (VarS x) (VarS y) = eqTy x y
68 type VarSem = Type -> [Type] -> Type -> Type
70 -- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v)
71 data VarV prov vs = forall v. VarV (Var prov vs v)
73 class LenVar var where
74 lenVar :: var prov vs a -> Len vs
75 instance LenVar Var where
76 lenVar VarZ{varZNext} = LenS varZNext
77 lenVar (VarS v) = LenS (lenVar v)
79 class LenVar var => AllocVars var where
80 allocVarsL :: Len len -> var prov vs x -> var prov (len ++ vs) x
81 allocVarsR :: Len len -> var prov vs x -> var prov (vs ++ len) x
82 instance AllocVars Var where
84 allocVarsL (LenS len) v = VarS (allocVarsL len v)
86 allocVarsR len VarZ{..} = VarZ{varZNext = addLen varZNext len, ..}
87 allocVarsR len (VarS v) = VarS (allocVarsR len v)
92 xVar prov xVS (x :: xK) ->
93 yVar prov yVS (y :: yK) ->
94 ( xVar prov (xVS ++ yVS) x
95 , yVar prov (xVS ++ yVS) y
98 ( allocVarsR (lenVar y) x
99 , allocVarsL (lenVar x) y
102 -- ** Type 'IndexVar'
104 -- | Index of a 'Var'.
107 indexVar :: Var prov vs v -> Int
109 indexVar (VarS v) = 1 Prelude.+ indexVar v
111 -- instance KindOf (Var prov vs) where
114 -- go :: forall vs2 aK a. Var prov vs2 (Proxy (a::aK)) -> TypeRep aK
115 -- go VarZ{varKind} = varKind
116 -- go (VarS v) = go v
119 type Vars prov vs = Map.Map Name (VarV prov vs)
121 lookupVar :: Name -> Vars prov vs -> Maybe (VarV prov vs)
122 lookupVar = Map.lookup
124 insertVar :: Name -> VarV prov vs -> Vars prov vs -> Vars prov vs
125 insertVar = Map.insert
129 -- | List of 'Var's, used to change the context of a 'Var'
130 -- when removing unused 'Var's.
131 data UsedVars oldVS prov newVS a where
132 UsedVarsZ :: UsedVars oldVS prov '[] a
134 Var prov oldVS (v :: vK) ->
135 UsedVars oldVS prov newVS a ->
136 UsedVars oldVS prov (Proxy (v :: vK) ': newVS) a
138 instance LenVar (UsedVars oldVS) where
139 lenVar UsedVarsZ = LenZ
140 lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS
143 Var prov oldVS (v :: vK) ->
144 UsedVars oldVS prov newVS a ->
145 Maybe (Var prov newVS (v :: vK))
146 lookupUsedVars _v UsedVarsZ = Nothing
147 lookupUsedVars v (UsedVarsS v' us) = do
154 { varZNext = lenVar us
157 Nothing -> VarS Data.Functor.<$> lookupUsedVars v us
161 UsedVars vs prov us a ->
162 Maybe (UsedVars vs prov (Proxy v ': us) a)
163 insertUsedVars v vs =
164 case lookupUsedVars v vs of
166 Nothing -> Just (UsedVarsS v vs)
168 -- | Remove unused 'Var's from the context.
170 Ty prov vs (a :: aK) ->
171 (forall newVS. Ty prov newVS (a :: aK) -> ret) ->
173 normalizeVarsTy ty k =
174 usedVarsOf UsedVarsZ ty $ \vs ->
177 goTy :: UsedVars oldVS prov newVS b -> Ty prov oldVS a -> Ty prov newVS a
178 goTy vs TyConst{..} = TyConst{tyConstLen = lenVar vs, ..}
179 goTy vs TyApp{..} = TyApp{tyAppFun = goTy vs tyAppFun, tyAppArg = goTy vs tyAppArg}
181 case tyVar `lookupUsedVars` vs of
182 Nothing -> Prelude.error "[BUG] normalizeVarsTy: impossible lookup fail"
183 Just v' -> TyVar{tyVar = v', ..}
184 goTy vs TyProv{..} = TyProv{tyUnProv = goTy vs tyUnProv, ..}
186 -- goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as
189 -- UsedVars src vs vs' ->
192 -- goTys _vs TysZ = TypesZ
193 -- goTys vs (TysS t ts) =
194 -- goTy vs t `TypesS`
197 -- * Class 'VarOccursIn'
199 -- | Test whether a given 'Var' occurs within @(t)@.
200 class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where
201 varOccursIn :: Var prov vs v -> t prov vs a -> Bool
203 -- * Class 'UsedVarsOf'
204 class UsedVarsOf t where
206 UsedVars vs prov oldVS a ->
208 (forall newVS. UsedVars vs prov newVS a -> ret) ->
213 -- Use a CUSK, because it's a polymorphically recursive type,
214 -- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
215 data Ty :: forall aK. Prov -> [Type] -> aK -> Type where
216 TyConst :: {tyConst :: Const a, tyConstLen :: Len vs} -> Ty prov vs a
217 TyVar :: {tyVar :: Var prov vs a, tyVarName :: Name} -> Ty prov vs a
218 TyApp :: {tyAppFun :: Ty prov vs f, tyAppArg :: Ty prov vs a} -> Ty prov vs (f a)
219 TyProv :: {tyProv :: prov, tyUnProv :: Ty prov vs a} -> Ty prov vs a
222 tyOfTypeRep :: Len vs -> TypeRep a -> Ty prov vs a
223 tyOfTypeRep len ty = case ty of
224 App f x -> TyApp{tyAppFun = tyOfTypeRep len f, tyAppArg = tyOfTypeRep len x}
225 constType -> TyConst{tyConst = constType, tyConstLen = len}
227 -- | Monomorphic 'Ty' from a 'Typeable'.
228 monoTy :: forall {aK} (a :: aK) prov. Typeable a => Ty prov '[] a
229 monoTy = tyOfTypeRep LenZ typeRep
231 aTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': vs) (a :: Type)
232 bTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': Proxy b ': vs) (b :: Type)
233 cTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : vs) (c :: Type)
234 dTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : Proxy d : vs) (d :: Type)
235 aTy = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "a"}
236 bTy = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "b"}
237 cTy = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "c"}
238 dTy = TyVar{tyVar = VarS $ VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "d"}
240 pattern SkipTyProv :: () => () => Ty prov vs a -> Ty prov vs a
241 pattern SkipTyProv ty <- (skipTyProv -> ty)
242 {-# COMPLETE SkipTyProv #-}
244 skipTyProv :: Ty prov vs a -> Ty prov vs a
245 skipTyProv TyProv{tyUnProv} = tyUnProv
250 forall k (fun :: k) prov vs.
260 , fun ~~ (arg -> res)
262 -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
267 pattern FUN arg res <-
273 { tyAppFun = SkipTyProv TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
279 (~>) :: Monoid prov => Ty prov vs a -> Ty prov vs b -> Ty prov vs (a -> b)
285 TyConst{tyConst = typeRep, tyConstLen = (lenVar arg)}
292 deriving instance Show prov => Show (Ty prov vs a)
294 -- type instance SourceOf (Ty vs src t) = src
295 instance LenVar Ty where
296 lenVar TyConst{tyConstLen} = tyConstLen
297 lenVar TyApp{tyAppFun} = lenVar tyAppFun
298 lenVar TyVar{tyVar} = lenVar tyVar
299 lenVar TyProv{tyUnProv} = lenVar tyUnProv
301 -- lenVars (TyFam l _f _as) = l
302 instance AllocVars Ty where
303 allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
304 allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
305 allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
306 allocVarsL len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsL len tyUnProv}
308 -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
310 allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
311 allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
312 allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
313 allocVarsR len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsR len tyUnProv}
315 -- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
317 instance VarOccursIn Ty where
318 varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
319 varOccursIn _v TyVar{} = False
320 varOccursIn _v TyConst{} = False
321 varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
322 varOccursIn v TyProv{..} = varOccursIn v tyUnProv
324 -- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
325 instance UsedVarsOf Ty where
326 usedVarsOf vs TyConst{} k = k vs
327 usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
328 usedVarsOf vs f $ \vs' ->
330 usedVarsOf vs TyVar{tyVar = v} k =
331 case insertUsedVars v vs of
334 usedVarsOf vs TyProv{tyUnProv} k = usedVarsOf vs tyUnProv k
336 -- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
340 -- | Existential for 'Type'.
341 data TyT prov vs = forall a. TyT (Ty prov vs a)
343 -- type instance SourceOf (TyT vs src) = src
344 instance Eq (TyT prov vs) where
345 TyT x == TyT y = isJust $ eqTy x y
346 instance Show prov => Show (TyT prov vs) where
347 showsPrec p (TyT x) = showsPrec p x
350 type Kind prov a = Ty prov '[] a
353 type KindK prov = TyT prov '[]
356 data TyVT prov = forall vs a. TyVT (Ty prov vs a)
358 deriving instance Show prov => Show (TyVT prov)
359 instance Eq (TyVT m) where
360 TyVT x == TyVT y = isJust (eqTy x' y')
362 (x', y') = appendVars x y
364 -- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
365 -- eqTy x y = eqTy (unSourced x) (unSourced y)
366 instance EqTy (Ty prov vs) (Ty prov vs) where
369 go :: forall xK xT yK yT. Ty prov vs (xT :: xK) -> Ty prov vs (yT :: yK) -> Maybe (xT :~~: yT)
370 go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
371 go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
372 go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
373 | Just HRefl <- go xF yF
374 , Just HRefl <- go xA yA =
376 go TyProv{tyUnProv = x} y = go x y
377 go x TyProv{tyUnProv = y} = go x y
380 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
381 -- | Just HRefl <- eqTypeRep xF yF
382 -- , Just HRefl <- eqTys xA yA
384 -- -- NOTE: 'TyFam' is expanded as much as possible.
385 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
386 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
389 data Tys (as :: [Type]) prov vs (a :: aK) where
390 TysZ :: Tys '[] prov vs a
391 TysS :: Ty prov vs a -> Tys as prov vs b -> Tys (Proxy a ': as) prov vs b
394 -- type instance SourceOf (Tys vs src ts) = src
395 -- instance ConstsOf (Tys prov vs ts) where
396 -- constsOf TysZ = Set.empty
397 -- constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
398 instance UsedVarsOf (Tys as) where
399 usedVarsOf vs TysZ k = k vs
400 usedVarsOf vs (TysS t ts) k =
401 usedVarsOf vs t $ \vs' ->
403 instance VarOccursIn (Tys as) where
404 varOccursIn _v TysZ = False
405 varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
407 -- ** Type family 'FunArg'
408 type family FunArg (fun :: Type) :: Type where
409 FunArg (q #> f) = FunArg f
412 -- ** Type family 'FunRes'
413 type family FunRes (fun :: Type) :: Type where
414 FunRes (q #> f) = FunRes f
417 -- -- | Return, when the given 'Type' is a function,
418 -- -- the argument of that function.
421 -- SourceInj (TyVT src) src =>
422 -- --Constable (->) =>
424 -- Maybe ( Type src tys (FunArg t)
425 -- , Type src tys (FunRes t) )
426 -- unTyFun ty_ini = go ty_ini
430 -- Maybe ( Type src tys (FunArg x)
431 -- , Type src tys (FunRes x) )
432 -- go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
433 -- | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
434 -- = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
435 -- go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
436 -- | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
438 -- go TyApp{} = Nothing
439 -- go TyConst{} = Nothing
440 -- go TyVar{} = Nothing
441 -- go TyFam{} = Nothing
444 forall kc (c :: kc) u.
446 -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
447 -- KindInjP (Ty_of_Type kc) =>
450 proj_ConstKi = eqTypeRep (typeRep @c)
454 -- | /Type constant/ to qualify a 'Type'.
455 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
457 -- | Qualify a 'Type'.
458 (#>) :: Monoid prov => Ty prov vs q -> Ty prov vs t -> Ty prov vs (q #> t)
460 -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
464 { tyAppFun = TyConst{tyConst = typeRep @(#>), tyConstLen = lenVar q}
472 -- NOTE: should actually be (-1)
473 -- to compose well with @infixr 0 (->)@
474 -- but this is not allowed by GHC.
478 -- | 'Constraint' union.
479 class ((x, y) :: Constraint) => x # y
481 instance ((x, y) :: Constraint) => x # y
483 -- | Unify two 'K.Constraint's.
484 (#) :: Monoid prov => Ty prov vs qx -> Ty prov vs qy -> Ty prov vs (qx # qy)
486 -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
490 { tyAppFun = TyConst{tyConst = typeRep @(#), tyConstLen = lenVar a}
499 class KindOf (ty :: Prov -> [Type] -> aK -> Type) where
500 -- | Return the kind of the given 'Var'.
503 ProvenanceKindOf ty prov =>
505 ty prov vs (a :: aK) ->
506 Kind prov (aK :: Type)
508 instance KindOf Var where
509 kindOf v@Var{varKind} = TyProv (provenanceKindOf v) varKind
510 instance KindOf Ty where
511 kindOf ty = TyProv (provenanceKindOf ty) (go ty)
515 Ty prov vs (a :: aK) ->
516 Kind prov (aK :: Type)
517 go TyConst{tyConst = constType :: Const (a :: aK)} =
518 tyOfTypeRep LenZ (typeRepKind constType)
519 go TyApp{tyAppFun = f} = case go f of
525 { tyAppFun = SkipTyProv TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
529 t -> Prelude.error $ "here: " <> show t
530 go TyVar{..} = varKind tyVar
531 go TyProv{..} = go tyUnProv
533 -- ** Class 'ProvenanceKindOf'
534 class ProvenanceKindOf (ty :: Prov -> [Type] -> aK -> Type) prov where
535 provenanceKindOf :: ty prov vs (a :: aK) -> prov
536 instance ProvenanceKindOf ty () where
537 provenanceKindOf _ = ()
538 instance ProvenanceKindOf Ty String where
539 provenanceKindOf = show
540 instance ProvenanceKindOf Var String where
541 provenanceKindOf = show
543 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam