Safe Haskell	None
Language	Haskell2010

Control.Monad.Foil.Internal.ValidNameBinders

Documentation

type family SubstInRepK (i :: TyVar d k) (atom :: Atom d k) (f :: LoT d -> Type) :: LoT d -> Type where ... Source #

Equations

SubstInRepK (i :: TyVar d k) (atom :: Atom d k) (V1 :: LoT d -> Type) = V1 :: LoT d -> Type
SubstInRepK (i :: TyVar d k) (atom :: Atom d k) (U1 :: LoT d -> Type) = U1 :: LoT d -> Type
SubstInRepK (i :: TyVar d k) (atom :: Atom d k) (M1 info c f :: LoT d -> Type) = M1 info c (SubstInRepK i atom f)
SubstInRepK (i :: TyVar d k) (atom :: Atom d k) (Field field :: LoT d -> Type) = Field (SubstInAtom i atom field)
SubstInRepK (i :: TyVar d k1) (atom :: Atom d k1) (f :: LoT d -> Type) = TypeError ((((('Text "cannot substitute variable" ':$$: ('Text " " ':<>: 'ShowType ('Var i))) ':$$: 'Text "with atom") ':$$: ('Text " " ':<>: 'ShowType atom)) ':$$: 'Text "in") ':$$: ('Text " " ':<>: 'ShowType f)) :: LoT d -> Type

type family SubstInAtom (i :: TyVar d k) (atom :: Atom d k) (f :: Atom d k1) :: Atom d k1 where ... Source #

Equations

SubstInAtom (i :: TyVar d k1) (atom :: Atom d k1) ('Var i :: Atom d k1) = atom
SubstInAtom (i :: TyVar d k) (atom :: Atom d k) ('Var j :: Atom d k1) = 'Var j
SubstInAtom (i :: TyVar d k) (atom :: Atom d k) ('Kon a :: Atom d k1) = 'Kon a :: Atom d k1
SubstInAtom (i :: TyVar d k) (atom :: Atom d k) (f ':@: x :: Atom d k2) = SubstInAtom i atom f ':@: SubstInAtom i atom x
SubstInAtom (i :: TyVar d k2) (atom :: Atom d k2) (atom' :: Atom d k3) = TypeError ((((('Text "cannot substitute variable" ':$$: ('Text " " ':<>: 'ShowType ('Var i))) ':$$: 'Text "with atom") ':$$: ('Text " " ':<>: 'ShowType atom)) ':$$: 'Text "in an atom") ':$$: ('Text " " ':<>: 'ShowType atom')) :: Atom d k3

type ShowKindedScope (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) = ShowScope oo n ll ':<>: 'Text " : S" Source #

type family ShowScope (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) :: ErrorMessage where ... Source #

Equations

ShowScope (oo :: Atom d s) (ll :: Atom d s) (ll :: Atom d s) = 'Text "innerScope"
ShowScope (oo :: Atom d s) (oo :: Atom d s) (ll :: Atom d s) = 'Text "outerScope"
ShowScope (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) = ShowScopeN 1 n

type family ShowScopeN (i :: Natural) (n :: Atom d s) :: ErrorMessage where ... Source #

Equations

ShowScopeN i ('Var ('VZ :: TyVar (s -> xs) s) :: Atom (s -> xs) s) = 'Text "scope" ':<>: 'ShowType i
ShowScopeN i ('Var ('VS x2 :: TyVar (x1 -> d) s) :: Atom (x1 -> d) s) = ShowScopeN (i + 1) ('Var x2)

type ShowSaturatedPatternType (pattern :: t) (oo :: Atom d s) (n :: Atom d s) (l :: Atom d s) (ll :: Atom d s) = ((('ShowType pattern ':<>: 'Text " ") ':<>: ShowScope oo n ll) ':<>: 'Text " ") ':<>: ShowScope oo l ll Source #

type family GInnerScopeOfAtom (msg :: ErrorMessage) (icon :: Nat) (ifield :: Nat) (pattern :: s -> s -> Type) (atom :: Atom d Type) (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) :: Atom d s where ... Source #

Equations

GInnerScopeOfAtom msg icon ifield (pattern :: s -> s -> Type) ((('Kon f :: Atom d (s -> s -> Type)) ':@: n) ':@: l :: Atom d Type) (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) = l
GInnerScopeOfAtom msg icon ifield (pattern :: s -> s -> Type) ((('Kon f :: Atom d (s -> s -> Type)) ':@: o) ':@: i :: Atom d Type) (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) = TypeError (((((((('Text "Unexpected Foil scope extension in the binder/pattern" ':$$: ('Text " " ':<>: ShowSaturatedPatternType f oo o i ll)) ':$$: 'Text "the binder/pattern tries to extend scope") ':$$: ('Text " " ':<>: ShowKindedScope oo o ll)) ':$$: 'Text "to scope") ':$$: ('Text " " ':<>: ShowKindedScope oo i ll)) ':$$: 'Text "but it is expected to extend the current (outer) scope") ':$$: ('Text " " ':<>: ShowKindedScope oo n ll)) ':$$: ShowLocalizeError msg icon ifield pattern oo ll) :: Atom d s
GInnerScopeOfAtom msg icon ifield (pattern :: s -> s -> Type) (atom :: Atom d Type) (oo :: Atom d s) (n :: Atom d s) (ll :: Atom d s) = n

type family SameInnerScope (msg :: ErrorMessage) (icon :: Nat) (pattern :: s -> s -> Type) (n :: Atom k s) (l :: Atom k s) :: Atom k s where ... Source #

Equations

SameInnerScope msg icon (pattern :: s -> s -> Type) (l :: Atom k s) (l :: Atom k s) = l

SameInnerScope msg icon (pattern :: s -> s -> Type) (n :: Atom d s) (l :: Atom d s) = TypeError (((((('Text "Unexpected extended (inner) Foil scope in the data type" ':$$: ('Text " " ':<>: ShowSaturatedPatternType pattern n n l l)) ':$$: 'Text "expecting extended (inner) scope to be") ':$$: ('Text " " ':<>: ShowKindedScope n l l)) ':$$: 'Text "but the inferred extended (inner) scope is") ':$$: ('Text " " ':<>: ShowKindedScope n n l)) ':$$: ShowLocalizeError msg icon 0 pattern n l) :: Atom d s

type family GValidNameBinders (pattern :: s -> s -> Type) (f :: LoT (s -> s -> Type) -> Type) where ... Source #

Equations

GValidNameBinders (pattern :: s -> s -> Type) (f :: LoT (s -> s -> Type) -> Type) = GInnerScopeOfRepK ('Text "") 0 0 pattern f (Var0 :: Atom (s -> s -> Type) s) (Var0 :: Atom (s -> s -> Type) s) (Var1 :: Atom (s -> s -> Type) s) ~ (Var1 :: Atom (s -> s -> Type) s)

type family AtomSucc (atom :: Atom d k1) :: Atom (k -> d) k1 where ... Source #

Equations

AtomSucc ('Var i :: Atom xs k1) = 'Var ('VS i :: TyVar (k -> xs) k1)

type family AtomUnSucc (msg :: ErrorMessage) (icon :: Nat) (pattern :: s -> s -> Type) (oo :: Atom d s) (ll :: Atom d s) (atom :: Atom (k -> d) k1) :: Atom d k1 where ... Source #

Equations

AtomUnSucc msg icon (pattern :: s -> s -> Type) (oo :: Atom d s) (ll :: Atom d s) ('Var ('VS i :: TyVar (k -> d) k1) :: Atom (k -> d) k1) = 'Var i
AtomUnSucc msg icon (pattern :: s -> s -> Type) (oo :: Atom d s) (ll :: Atom d s) ('Var ('VZ :: TyVar (k1 -> d) k1) :: Atom (k1 -> d) k1) = TypeError ('Text "Intermediate scope escapes existential quantification for data type" ':$$: ShowLocalizeError msg icon 0 pattern oo ll) :: Atom d k1

type family First (x :: Atom d k1) (y :: Atom d1 k2) :: Atom d k1 where ... Source #

Equations

First ('Var x :: Atom d1 k2) ('Var y :: Atom d2 k3) = 'Var x

type family AndShowFieldNumber (ifield :: Natural) (msg :: ErrorMessage) :: ErrorMessage where ... Source #

Equations

AndShowFieldNumber 0 msg = msg
AndShowFieldNumber n msg = ('Text "when checking field number " ':<>: 'ShowType n) ':$$: msg

type family AndShowConNumber (icon :: Natural) (msg :: ErrorMessage) :: ErrorMessage where ... Source #

Equations

AndShowConNumber 0 msg = msg
AndShowConNumber n msg = ('Text "when checking constructor number " ':<>: 'ShowType n) ':$$: msg

type AndShowDataType (pattern :: t) (n :: Atom d s) (l :: Atom d s) (msg :: ErrorMessage) = ('Text "when tracking Foil scopes for the data type" ':$$: ('Text " " ':<>: ShowSaturatedPatternType pattern n n l l)) ':$$: msg Source #

type ShowLocalizeError (msg :: ErrorMessage) (icon :: Natural) (ifield :: Natural) (pattern :: t) (o :: Atom d s) (l :: Atom d s) = AndShowFieldNumber ifield (AndShowConNumber icon (AndShowDataType pattern o l msg)) Source #

type family CountCons (f :: k -> Type) :: Natural where ... Source #

Equations

CountCons (f :+: g :: k -> Type) = CountCons f + CountCons g
CountCons (M1 C c f :: k -> Type) = 1

type family CountFields (f :: k -> Type) :: Natural where ... Source #

Equations

CountFields (f :*: g :: k -> Type) = CountFields f + CountFields g
CountFields (M1 S c f :: k -> Type) = 1

type family GInnerScopeOfRepK (msg :: ErrorMessage) (icon :: Nat) (ifield :: Nat) (pattern :: s -> s -> Type) (f :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) :: Atom k s where ... Source #

Equations

GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (V1 :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = l
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (U1 :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = n
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (M1 C c f :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = GInnerScopeOfRepK msg icon 1 pattern f o n l
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (M1 D c f :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = GInnerScopeOfRepK msg 1 ifield pattern f o n l
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (M1 i c f :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = GInnerScopeOfRepK msg icon ifield pattern f o n l
GInnerScopeOfRepK msg icon ifield (pattern :: k1 -> k1 -> Type) (f :+: g :: LoT d -> Type) (o :: Atom d k1) (n :: Atom d k1) (l :: Atom d k1) = First (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg icon ifield pattern f o n l) l) (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg (icon + CountCons f) ifield pattern g o n l) l)
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (f :*: g :: LoT k -> Type) (o :: Atom k s) (n :: Atom k s) (l :: Atom k s) = GInnerScopeOfRepK msg icon (ifield + CountFields f) pattern g o (GInnerScopeOfRepK msg icon ifield pattern f o n l) l
GInnerScopeOfRepK msg icon ifield (pattern :: k2 -> k2 -> Type) (('Var i :~~: 'Var j) :=>: f :: LoT d -> Type) (o :: Atom d k2) (n :: Atom d k2) (l :: Atom d k2) = GInnerScopeOfRepK msg icon ifield pattern (SubstInRepK i ('Var j) f) (SubstInAtom i ('Var j) o) (SubstInAtom i ('Var j) n) (SubstInAtom i ('Var j) l)
GInnerScopeOfRepK msg icon ifield (pattern :: k1 -> k1 -> Type) (Exists k f :: LoT d -> Type) (o :: Atom d k1) (n :: Atom d k1) (l :: Atom d k1) = AtomUnSucc msg icon pattern o l (GInnerScopeOfRepK msg icon ifield pattern f (AtomSucc o :: Atom (k -> d) k1) (AtomSucc n :: Atom (k -> d) k1) (AtomSucc l :: Atom (k -> d) k1))
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (Field atom :: LoT d -> Type) (o :: Atom d s) (n :: Atom d s) (l :: Atom d s) = GInnerScopeOfAtom msg icon ifield pattern atom o n l
GInnerScopeOfRepK msg icon ifield (pattern :: s -> s -> Type) (f :: LoT d -> Type) (o :: Atom d s) (n :: Atom d s) (l :: Atom d s) = TypeError (('Text "Unsupported structure in a binder/pattern" ':$$: ('Text " " ':<>: 'ShowType f)) ':$$: ShowLocalizeError msg icon 0 pattern n l) :: Atom d s

type family PutBackLoT (i :: TyVar d s) (c :: s) (bs :: LoT k) :: LoT k where ... Source #

Equations

PutBackLoT ('VZ :: TyVar (k1 -> xs) k1) (c :: k1) (b ':&&: bs :: LoT (k1 -> ks)) = c ':&&: bs
PutBackLoT ('VS x2 :: TyVar (x1 -> d) s) (c :: s) (b ':&&: bs :: LoT (k1 -> ks)) = b ':&&: PutBackLoT x2 c bs