1 {-# language ConstraintKinds #-}
2 {-# LANGUAGE AllowAmbiguousTypes #-}
3 {-# LANGUAGE PartialTypeSignatures #-}
4 {-# LANGUAGE ImpredicativeTypes #-}
5 {-# LANGUAGE LiberalTypeSynonyms #-}
7 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
8 {-# LANGUAGE TypeInType #-}
9 {-# LANGUAGE PolyKinds #-}
10 {-# LANGUAGE NoMonomorphismRestriction #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# LANGUAGE UndecidableSuperClasses #-}
13 {-# OPTIONS_GHC -fno-warn-orphans #-}
14 module Language.Symantic.Typing.Type
15 ( module Language.Symantic.Typing.Type
22 import Control.Applicative (Alternative(..))
23 import Data.Maybe (isJust)
25 import Data.Semigroup ((<>))
27 import Data.Type.Equality
29 import qualified Data.Kind as K
30 import qualified Data.Set as Set
32 import Language.Symantic.Grammar
33 import Language.Symantic.Typing.List
34 import Language.Symantic.Typing.Kind
35 import Language.Symantic.Typing.Variable
38 data Type (src::K.Type) (vs::[K.Type]) (t::kt) where
39 TyConst :: src -> Len vs
42 TyApp :: src -> Type src vs f
45 -- NOTE: @f a@ decomposition made possible
46 -- at the cost of requiring @TypeInType@.
47 TyVar :: src -> NameVar
50 TyFam :: src -> Len vs
53 -> Type src vs (Fam fam hs)
55 TyPi :: src -> Type src (arg ': vs) res
56 -> Type (Pi arg res) src vs
57 TyQuant :: src -> NameHint
59 -> (forall (v::kv). Type src vs v -> TypeK src vs k)
61 TyEq :: src -> Type x src vs
63 -> Type (x #~ y) src vs
66 instance Source src => Eq (Type src vs t) where
67 x == y = isJust $ eqType x y
68 instance Inj_Source (TypeVT src) src => TestEquality (Type src vs) where
71 type instance SourceOf (Type src vs t) = src
72 instance Source src => Sourced (Type src vs t) where
73 sourceOf (TyConst src _l _c) = src
74 sourceOf (TyApp src _f _a) = src
75 sourceOf (TyVar src _n _v) = src
76 sourceOf (TyFam src _l _f _as) = src
78 setSource (TyConst _src l c) src = TyConst src l c
79 setSource (TyApp _src f a) src = TyApp src f a
80 setSource (TyVar _src n v) src = TyVar src n v
81 setSource (TyFam _src l f as) src = TyFam src l f as
83 instance Inj_Source (TypeVT src) src => KindOf (Type src vs) where
84 kindOf t = kindOfType t `source` TypeVT t
86 instance ConstsOf (Type src vs t) where
87 constsOf (TyConst _src _len c) = Set.singleton $ ConstC c
88 constsOf TyVar{} = Set.empty
89 constsOf (TyApp _src f a) = constsOf f `Set.union` constsOf a
90 constsOf (TyFam _src _len fam as) = constsOf fam `Set.union` constsOf as
92 type instance VarsOf (Type src vs t) = vs
93 instance LenVars (Type src vs t) where
94 lenVars (TyConst _src len _c) = len
95 lenVars (TyApp _src f _a) = lenVars f
96 lenVars (TyVar _src _n v) = lenVars v
97 lenVars (TyFam _src l _f _as) = l
98 instance UsedVarsOf (Type src vs t) where
99 usedVarsOf vs TyConst{} k = k vs
100 usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
101 usedVarsOf vs (TyApp _src f a) k =
102 usedVarsOf vs f $ \vs' ->
104 usedVarsOf vs (TyVar _src _n v) k =
105 case insertUsedVars v vs of
108 instance VarOccursIn (Type src vs t) where
109 varOccursIn v (TyVar _src _n v') | Just{} <- v `eqVarKi` v' = False
110 varOccursIn _v TyVar{} = False
111 varOccursIn _v TyConst{} = False
112 varOccursIn v (TyApp _src f a) = varOccursIn v f || varOccursIn v a
113 varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
114 instance AllocVars (Type src) where
115 allocVarsL len (TyConst src l c) = TyConst src (addLen len l) c
116 allocVarsL len (TyApp src f a) = TyApp src (allocVarsL len f) (allocVarsL len a)
117 allocVarsL len (TyVar src n v) = TyVar src n $ allocVarsL len v
118 allocVarsL len (TyFam src l f as) = TyFam src (addLen len l) f $ allocVarsL len `mapTys` as
120 allocVarsR len (TyConst src l c) = TyConst src (addLen l len) c
121 allocVarsR len (TyApp src f a) = TyApp src (allocVarsR len f) (allocVarsR len a)
122 allocVarsR len (TyVar src n v) = TyVar src n $ allocVarsR len v
123 allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as
125 -- | Like 'TyConst', but using 'noSource' and 'inj_Const'.
127 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
129 forall kc (c::kc) src vs.
133 Inj_KindP (Ty_of_Type kc) =>
134 Type_of_Ty (Ty_of_Type kc) ~ kc =>
136 tyConst = TyConst noSource inj_Len inj_Const
137 -- NOTE: The forall brings @c@ first in the type variables,
138 -- which is convenient to use @TypeApplications@.
140 -- | Like 'TyConst', but using 'noSource' and 'inj_Const'.
142 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
144 forall kc (c::kc) src vs.
147 Inj_KindP (Ty_of_Type kc) =>
148 Type_of_Ty (Ty_of_Type kc) ~ kc =>
151 tyConstLen len = TyConst noSource len inj_Const
153 -- | Like 'TyApp', but using 'noSource'.
159 tyApp = TyApp noSource
162 -- | Like 'TyVar', but using 'noSource'.
168 tyVar = TyVar noSource
170 -- | Like 'TyFam', but using 'noSource'.
172 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
174 forall kc (c::kc) as vs src.
178 Inj_KindP (Ty_of_Type kc) =>
179 Type_of_Ty (Ty_of_Type kc) ~ kc =>
181 Type src vs (Fam c as)
182 tyFam = TyFam noSource inj_Len (inj_Const @c)
184 -- | Qualify a 'Type'.
191 Type src vs (q #> t)) ->
194 case proveConstraint q of
195 Just Dict -> f Dict t
200 -- | Existential 'Type' of a known 'Kind'.
201 data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t)
202 type instance SourceOf (TypeK src vs ki) = src
203 type instance VarsOf (TypeK src vs ki) = vs
204 instance Source src => Eq (TypeK src vs ki) where
205 TypeK x == TypeK y = isJust $ eqType x y
208 -- | Existential for 'Type'.
209 data TypeT src vs = forall t. TypeT (Type src vs t)
210 type instance SourceOf (TypeT src vs) = src
211 type instance VarsOf (TypeT src vs) = vs
212 instance Inj_Source (TypeVT src) src => Eq (TypeT src vs) where
213 TypeT x == TypeT y = isJust $ eqTypeKi x y
216 -- | Existential polymorphic 'Type'.
217 data TypeVT src = forall vs t. TypeVT (Type src vs t)
218 type instance SourceOf (TypeVT src) = src
219 instance Source src => Eq (TypeVT src) where
220 TypeVT x == TypeVT y =
221 let (x', y') = appendVars x y in
222 isJust $ eqTypeKi x' y'
225 -- | /Type constant/.
226 data Const src (c::kc) where
231 type instance SourceOf (Const src c) = src
232 instance ConstsOf (Const src c) where
233 constsOf = Set.singleton . ConstC
234 instance Inj_Source (ConstC src) src => KindOf (Const src) where
235 kindOf c@(Const kc) = kc `source` ConstC c
237 kindOfConst :: Const src (t::kt) -> Kind src kt
238 kindOfConst (Const kc) = kc
240 -- ** Class 'Constable'
244 , ClassInstancesFor c
250 , ClassInstancesFor c
254 -- ** Class 'ConstsOf'
255 -- | Return the 'Const's used by something.
256 class ConstsOf a where
257 constsOf :: a -> Set (ConstC (SourceOf a))
259 -- ** Class 'FixityOf'
260 -- | Return the 'Fixity' of something.
261 class FixityOf (c::kc) where
262 fixityOf :: proxy c -> Fixity
263 fixityOf _c = Fixity2 $ infixN5
264 instance FixityOf (c::K.Type) where
265 fixityOf _c = Fixity2 $ infixN5
266 instance FixityOf (c::K.Constraint) where
267 fixityOf _c = Fixity2 $ infixN5
270 instance Show (Const src c) where
271 showsPrec p c@Const{} = showsPrec p $ typeRep c
275 = forall c. ConstC (Const src c)
276 instance Eq (ConstC src) where
277 ConstC x == ConstC y = isJust $ x `eqConstKi` y
278 instance Ord (ConstC src) where
279 ConstC x `compare` ConstC y = x `ordConst` y
282 -- | The function 'Type' @(->)@,
283 -- with an infix notation more readable.
290 (~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b
292 instance FixityOf (->) where
293 fixityOf _c = Fixity2 $ infixR 0
294 {- NOTE: defined in Lib.Function
295 instance ClassInstancesFor (->)
296 instance TypeInstancesFor (->)
299 -- ** Type family 'FunArg'
300 type family FunArg (fun::K.Type) :: K.Type where
301 FunArg (q #> f) = FunArg f
304 -- ** Type family 'FunRes'
305 type family FunRes (fun::K.Type) :: K.Type where
306 FunRes (q #> f) = FunRes f
309 -- | Return, when the given 'Type' is a function,
310 -- the argument of that function.
313 Inj_Source (TypeVT src) src =>
316 Maybe ( Type src tys (FunArg t)
317 , Type src tys (FunRes t) )
318 unTyFun ty_ini = go ty_ini
322 Maybe ( Type src tys (FunArg x)
323 , Type src tys (FunRes x) )
324 go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
325 | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
326 = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini))
327 go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
328 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
331 go TyConst{} = Nothing
336 -- | /Type constant/ to qualify a 'Type'.
337 data (#>) (q::K.Constraint) (a::K.Type)
338 instance FixityOf (#>) where
339 fixityOf _c = Fixity2 $ infixR 0
340 instance ClassInstancesFor (#>)
341 instance TypeInstancesFor (#>)
348 (#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b
350 -- NOTE: should actually be (-1)
351 -- to compose well with @infixr 0 (->)@
352 -- but this is not allowed by GHC.
355 -- | 'K.Constraint' union.
356 class (x, y) => x # y
357 instance (x, y) => x # y
358 instance FixityOf (#) where
359 fixityOf _c = Fixity2 $ infixB SideL 1
360 instance ClassInstancesFor (#) where
361 proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1)
362 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c
363 , Just Dict <- proveConstraint q0
364 , Just Dict <- proveConstraint q1
366 proveConstraintFor _c _q = Nothing
367 instance TypeInstancesFor (#)
373 Type src vs (qx # qy)
374 (#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
380 Type src vs (()::K.Constraint)
381 noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) inj_Len
386 Type src vs (()::K.Constraint)
387 noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)
389 instance ClassInstancesFor (()::K.Constraint) where
390 proveConstraintFor _c q
391 | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q
393 proveConstraintFor _c _q = Nothing
394 instance TypeInstancesFor (()::K.Constraint)
397 -- | /Type equality/ 'K.Constraint'.
398 class (x ~ y) => x #~ y
399 instance (x ~ y) => x #~ y
400 instance FixityOf (#~) where
401 fixityOf _ = Fixity2 $ infixB SideL 0
405 ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where
406 proveConstraintFor _c (TyApp _ (TyApp _ c a) b)
407 | Just HRefl <- proj_ConstKiTy @(k -> k -> K.Constraint) @(#~) c
408 , Just Refl <- eqType a b
410 proveConstraintFor _c _q = Nothing
411 instance TypeInstancesFor (#~)
418 Type src vs (a :: k) ->
419 Type src vs (b :: k) ->
421 (#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b
430 Const src ((#~)::k -> k -> K.Constraint)
431 const_EqTy = inj_Const @(#~)
434 -- | /Type equality/.
437 Type src tys (x::k) ->
438 Type src tys (y::k) ->
440 eqType x y | Just HRefl <- eqTypeKi x y = Just Refl
441 eqType _x _y = Nothing
443 -- | /Heterogeneous type equality/:
444 -- return two proofs when two 'Type's are equals:
445 -- one for the type and one for the kind.
448 Type src tys (x::kx) ->
449 Type src tys (y::ky) ->
451 eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y
452 eqTypeKi (TyVar _sx _nx x) (TyVar _sy _ny y) = eqVarKi x y
453 eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay)
454 | Just HRefl <- eqTypeKi fx fy
455 , Just HRefl <- eqTypeKi ax ay
457 eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
458 | Just HRefl <- eqConstKi fx fy
459 , Just HRefl <- eqTypes ax ay
461 -- NOTE: 'TyFam' is expanded as much as possible.
462 eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y
463 eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y)
464 eqTypeKi _x _y = Nothing
471 eqTypes TypesZ TypesZ = Just HRefl
472 eqTypes (x `TypesS` sx) (y `TypesS` sy)
473 | Just HRefl <- eqTypeKi x y
474 , Just HRefl <- eqTypes sx sy
476 eqTypes _x _y = Nothing
479 -- | Compare two 'Type's.
482 Type src tys (x::kx) ->
483 Type src tys (y::ky) ->
485 -- NOTE: 'TyFam' is expanded as much as possible.
486 ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay
487 ordType x@TyFam{} y = ordType (expandFam x) y
488 ordType x y@TyFam{} = ordType x (expandFam y)
489 ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y
490 ordType TyConst{} _y = LT
491 ordType _x TyConst{} = GT
492 ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y
493 ordType TyVar{} _y = LT
494 ordType _x TyVar{} = GT
495 ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy
496 -- ordType TyApp{} _y = LT
497 -- ordType _x TyApp{} = GT
504 ordTypes TypesZ TypesZ = EQ
505 ordTypes TypesZ TypesS{} = LT
506 ordTypes TypesS{} TypesZ = GT
507 ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy
510 -- | Captures the proof of a 'K.Constraint'
511 -- (and its dictionaries when it contains type classes):
512 -- pattern matching on the 'Dict' constructor
513 -- brings the 'K.Constraint' into scope.
517 -- ** Class 'ClassInstancesFor'
518 class ClassInstancesFor c where
524 proveConstraintFor _c _q = Nothing
526 proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
527 proveConstraint q = foldr proj Nothing $ constsOf q
528 where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)
535 Inj_KindP (Ty_of_Type (K c)) =>
536 Type_of_Ty (Ty_of_Type (K c)) ~ K c =>
538 inj_Const = Const $ inj_KindP (Proxy @(Ty_of_Type (K c))) noSource
549 {- XXX: not working because of GHC's #12933
553 (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>
557 proj_ConstKi (Const ku) = do
558 Refl <- eqKind ku $ inj_Kind @(K c) @()
563 -- | Like 'proj_ConstKi', but with kind equality already known.
569 proj_Const Const{} = eqT
571 -- | Like 'proj_Const', but on a 'Type'.
577 proj_ConstTy (TyConst _src _len Const{}) = eqT
578 proj_ConstTy _ = Nothing
580 -- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely,
581 -- when used multiple times in the same pattern match,
582 -- because of GHC's #12933.
584 forall kc (c::kc) u src.
586 (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
587 Inj_KindP (Ty_of_Type kc) =>
590 proj_ConstKi (Const ku) = do
591 Refl <- eqKind ku $ inj_KindP (Proxy @(Ty_of_Type kc)) ()
595 -- | Like 'proj_ConstKi', but on a 'Type'.
597 forall kc (c::kc) u src vs.
599 (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
600 Inj_KindP (Ty_of_Type kc) =>
603 proj_ConstKiTy (TyConst _src _len (Const ku)) = do
604 Refl <- eqKind ku $ inj_KindP (Proxy @(Ty_of_Type kc)) ()
607 proj_ConstKiTy _ = Nothing
610 Const src_x (x::k) ->
611 Const src_y (y::k) ->
613 eqConst (Const _kx) (Const _ky) = eqT
614 instance Eq (Const src c) where
615 x == y = isJust $ eqConstKi x y
616 instance Ord (Const src c) where
620 forall src_x src_y kx ky x y.
621 Const src_x (x::kx) ->
622 Const src_y (y::ky) ->
624 eqConstKi (Const kx) (Const ky)
625 | Just Refl <- eqKind kx ky
626 , Just (Refl::x:~:y) <- eqT
628 eqConstKi _x _y = Nothing
631 forall src_x src_y kx ky x y.
632 Const src_x (x::kx) ->
633 Const src_y (y::ky) ->
635 ordConst x@Const{} y@Const{} =
636 typeRep x `compare` typeRep y
640 Type src tys (t::kt) ->
642 normalizeQualsTy = go
646 Type src tys (a::ka) ->
649 go (TyApp s1 (TyApp s0 f q0) q1)
650 | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f
652 , TypeK q1' <- go q1 =
653 case (proveConstraint q0', proveConstraint q1') of
654 (Just{}, Just{}) -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0
655 (Just{}, Nothing) -> TypeK q1'
656 (Nothing, Just{}) -> TypeK q0'
657 (Nothing, Nothing) ->
658 case q0' `ordType` q1' of
659 LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1'
661 GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0'
663 go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t))
664 | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0
665 , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1
667 , TypeK q1' <- go q1 =
668 case (proveConstraint q0', proveConstraint q1') of
669 (Just{}, Just{}) -> TypeK t
670 (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t
671 (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t
672 (Nothing, Nothing) ->
673 case q0' `ordType` q1' of
675 let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in
676 TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t
677 EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t
679 let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in
680 TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t
682 go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
683 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c =
684 case proveConstraint q of
692 | Just Refl <- KiConstraint () `eqKind` kindOfType q
693 = case proveConstraint q of
694 Just{} -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q
699 = TypeK $ TyApp src f' a'
700 go t@TyFam{} = go (expandFam t)
701 go t@TyConst{} = TypeK t
702 go t@TyVar{} = TypeK t
704 -- * Type family 'Fam'
705 -- | Apply the /type family/ selected by @fam@
706 -- to a list of types (within a 'Proxy').
708 -- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s.
709 type family Fam (fam::k) (hs::[K.Type]) :: k
710 -- type family FamKi fam :: K.Type
712 -- ** Class 'TypeInstancesFor'
713 class TypeInstancesFor (c::kc) where
720 -> Maybe (Type src vs (Fam fam ts))
721 expandFamFor _c _len _fam _as = Nothing
723 -- ** Class 'ExpandFam'
724 class ExpandFam a where
725 expandFam :: Source (SourceOf a) => a -> a
726 instance ExpandFam (Type src vs t) where
727 expandFam t@TyConst{} = t
728 expandFam t@TyVar{} = t
729 expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a)
730 expandFam t@(TyFam _src len fam as) =
731 case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of
733 Just t' -> expandFam t'
734 where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as)
735 -- XXX: this can loop…
737 -- | Like 'kindOf' but keep the old 'Source'.
738 kindOfType :: Type src vs (t::kt) -> Kind src kt
739 kindOfType (TyConst _src _l c) = kindOfConst c
740 kindOfType (TyApp _src f _a) =
742 KiFun _src_kf _kx kf -> kf
743 kindOfType (TyVar _src _n v) = kindOfVar v
744 kindOfType (TyFam _src _len fam _as) = kindOfConst fam
746 -- | Remove unused 'Var's from ther context.
748 Type src vs (t::kt) ->
749 (forall vs'. Type src vs' (t::kt) -> ret) -> ret
750 normalizeVarsTy ty k =
751 usedVarsOf UsedVarsZ ty $ \vs ->
755 UsedVars src vs vs' ->
758 goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c
759 goTy vs (TyApp src f a) = TyApp src (goTy vs f) (goTy vs a)
760 goTy vs (TyVar src n v) =
761 case v `lookupUsedVars` vs of
762 Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail"
763 Just v' -> TyVar src n v'
764 goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as
767 UsedVars src vs vs' ->
770 goTys _vs TypesZ = TypesZ
771 goTys vs (TypesS t ts) =
776 data Types src vs (ts::[K.Type]) where
777 TypesZ :: Types src vs '[]
778 TypesS :: Type src vs t
780 -> Types src vs (Proxy t ': ts)
783 type instance SourceOf (Types src vs ts) = src
784 instance ConstsOf (Types src vs ts) where
785 constsOf TypesZ = Set.empty
786 constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts
787 type instance VarsOf (Types src vs ts) = vs
788 instance UsedVarsOf (Types src vs ts) where
789 usedVarsOf vs TypesZ k = k vs
790 usedVarsOf vs (TypesS t ts) k =
791 usedVarsOf vs t $ \vs' ->
793 instance VarOccursIn (Types src vs ts) where
794 varOccursIn _v TypesZ = False
795 varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts
798 (forall kt (t::kt). Type src vs t -> Type src vs' t) ->
801 mapTys _f TypesZ = TypesZ
802 mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts
805 (forall k (t::k). Type src vs t -> acc -> acc) ->
806 Types src vs ts -> acc -> acc
807 foldlTys _f TypesZ acc = acc
808 foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)