Data.Generics.Internal.Families.Changing

Documentation

type Indexed t = Indexed' t 0

type family Infer (s :: *) (a' :: *) (b :: *) :: * where ...

Equations

Infer (s a) a' b = ReplaceArgs (s a) (Unify a' b)

Infer s _ _ = s

data PTag

Constructors

PTag

type family P :: Nat -> k -> PTag -> k

type family LookupParam (a :: k) (p :: Nat) :: Maybe Nat where ...

Equations

LookupParam (param (n :: Nat)) m = 'Nothing

LookupParam (a (_ (m :: Nat))) n = IfEq m n ('Just 0) (MaybeAdd (LookupParam a n) 1)

LookupParam (a _) n = MaybeAdd (LookupParam a n) 1

LookupParam a _ = 'Nothing

type family ArgAt (t :: k) (n :: Nat) :: j where ...

Equations

ArgAt (t a) 0 = a

ArgAt (t a) n = ArgAt t (n - 1)

type family ArgCount (t :: k) :: Nat where ...

Equations

ArgCount (f a) = 1 + ArgCount f

ArgCount a = 0

class UnifyHead (a :: k) (b :: k)

Ensure that the types a and b are both applications of the same constructor. The arguments may be different.

Instances

a ~ b => UnifyHead (a :: k) (b :: k)

Defined in Data.Generics.Internal.Families.Changing

(gb ~ g b, UnifyHead f g) => UnifyHead (f a :: k1) (gb :: k1)

Defined in Data.Generics.Internal.Families.Changing