Hyper.Class.Infer

Documentation

type family InferOf (t :: HyperType) :: HyperType

InferOf e is the inference result of e.

Most commonly it is an inferred type, using

type instance InferOf MyTerm = ANode MyType

But it may also be other things, for example:

• An inferred value (for types inside terms)
• An inferred type together with a scope

Instances

type InferOf (App e)

Defined in Hyper.Type.AST.App

type InferOf (App e) = ANode (TypeOf e)

type InferOf (Rec1 h)

Defined in Hyper.Class.Infer

type InferOf (Rec1 h) = InferOf h

type InferOf (HCompose Prune t)

Defined in Hyper.Type.Prune

type InferOf (HCompose Prune t) = InferOf t

type InferOf (Var _1 t)

Defined in Hyper.Type.AST.Var

type InferOf (Var _1 t) = ANode (TypeOf t)

type InferOf (Scheme _1 t)

Defined in Hyper.Type.AST.Scheme

type InferOf (Scheme _1 t) = HFlip GTerm t

type InferOf (TypeSig _1 t)

Defined in Hyper.Type.AST.TypeSig

type InferOf (TypeSig _1 t) = InferOf t

type InferOf (FromNom _1 e)

Defined in Hyper.Type.AST.Nominal

type InferOf (FromNom _1 e) = FuncType (TypeOf e)

type InferOf (ToNom n e)

Defined in Hyper.Type.AST.Nominal

type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))

type InferOf (Let _1 e)

Defined in Hyper.Type.AST.Let

type InferOf (Let _1 e) = InferOf e

type InferOf (Lam _1 t)

Defined in Hyper.Type.AST.Lam

type InferOf (Lam _1 t) = ANode (TypeOf t)

type InferOf (a :+: _1)

Defined in Hyper.Class.Infer

type InferOf (a :+: _1) = InferOf a

type InferOf (TypedLam _1 _2 e)

Defined in Hyper.Type.AST.TypedLam

type InferOf (TypedLam _1 _2 e) = ANode (TypeOf e)

type InferOf (M1 _1 _2 h)

Defined in Hyper.Class.Infer

type InferOf (M1 _1 _2 h) = InferOf h

class (Monad m, HFunctor t) => Infer m t where

Infer m t enables infer to perform type-inference for t in the Monad m.

The inferContext method represents the following constraints on t:

• HNodesConstraint (InferOf t) (Unify m) - The child nodes of the inferrence can unify in the m Monad
• HNodesConstraint t (Infer m) - Infer m is also available for child nodes

It replaces context for the Infer class to avoid UndecidableSuperClasses.

Instances usually don't need to implement this method as the default implementation works for them, but infinitely polymorphic trees such as Scope do need to implement the method, because the required context is infinite.

Minimal complete definition

Nothing

Methods

inferBody :: (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)

Infer the body of an expression given the inference actions for its child nodes.

default inferBody :: (Generic1 t, Infer m (Rep1 t), InferOf t ~ InferOf (Rep1 t)) => (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)

inferContext :: proxy0 m -> proxy1 t -> Dict (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m))

default inferContext :: (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m)) => proxy0 m -> proxy1 t -> Dict (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m))

Instances

(Infer m expr, HasInferredType expr, HSubset' (TypeOf expr) (FuncType (TypeOf expr)), UnifyGen m (TypeOf expr)) => Infer m (App expr)

Defined in Hyper.Type.AST.App

Methods

inferBody :: forall (h :: AHyperType -> Type). (App expr # InferChild m h) -> m (App expr # h, InferOf (App expr) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (App expr) -> Dict (HNodesConstraint (App expr) (Infer m), HNodesConstraint (InferOf (App expr)) (UnifyGen m))

Infer m h => Infer m (Rec1 h)

Defined in Hyper.Class.Infer

Methods

inferBody :: forall (h0 :: AHyperType -> Type). (Rec1 h # InferChild m h0) -> m (Rec1 h # h0, InferOf (Rec1 h) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (Rec1 h) -> Dict (HNodesConstraint (Rec1 h) (Infer m), HNodesConstraint (InferOf (Rec1 h)) (UnifyGen m))

(Infer m t, HPointed (InferOf t), HTraversable (InferOf t), HNodesConstraint t (HComposeConstraint1 (Infer m) Prune)) => Infer m (HCompose Prune t)

Defined in Hyper.Type.Prune

Methods

inferBody :: forall (h :: AHyperType -> Type). (HCompose Prune t # InferChild m h) -> m (HCompose Prune t # h, InferOf (HCompose Prune t) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (HCompose Prune t) -> Dict (HNodesConstraint (HCompose Prune t) (Infer m), HNodesConstraint (InferOf (HCompose Prune t)) (UnifyGen m))

(UnifyGen m (TypeOf expr), HasScope m (ScopeOf expr), VarType v expr, Monad m) => Infer m (Var v expr)

Defined in Hyper.Type.AST.Var

Methods

inferBody :: forall (h :: AHyperType -> Type). (Var v expr # InferChild m h) -> m (Var v expr # h, InferOf (Var v expr) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (Var v expr) -> Dict (HNodesConstraint (Var v expr) (Infer m), HNodesConstraint (InferOf (Var v expr)) (UnifyGen m))

(Monad m, HasInferredValue typ, UnifyGen m typ, HTraversable varTypes, HNodesConstraint varTypes (MonadInstantiate m), RTraversable typ, Infer m typ) => Infer m (Scheme varTypes typ)

Defined in Hyper.Type.AST.Scheme

Methods

inferBody :: forall (h :: AHyperType -> Type). (Scheme varTypes typ # InferChild m h) -> m (Scheme varTypes typ # h, InferOf (Scheme varTypes typ) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (Scheme varTypes typ) -> Dict (HNodesConstraint (Scheme varTypes typ) (Infer m), HNodesConstraint (InferOf (Scheme varTypes typ)) (UnifyGen m))

(MonadScopeLevel m, HasInferredType term, HasInferredValue (TypeOf term), HTraversable vars, HTraversable (InferOf term), HNodesConstraint (InferOf term) (UnifyGen m), HNodesConstraint vars (MonadInstantiate m), UnifyGen m (TypeOf term), Infer m (TypeOf term), Infer m term) => Infer m (TypeSig vars term)

Defined in Hyper.Type.AST.TypeSig

Methods

inferBody :: forall (h :: AHyperType -> Type). (TypeSig vars term # InferChild m h) -> m (TypeSig vars term # h, InferOf (TypeSig vars term) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (TypeSig vars term) -> Dict (HNodesConstraint (TypeSig vars term) (Infer m), HNodesConstraint (InferOf (TypeSig vars term)) (UnifyGen m))

(Infer m expr, HasNominalInst nomId (TypeOf expr), MonadNominals nomId (TypeOf expr) m, HTraversable (NomVarTypes (TypeOf expr)), HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m), UnifyGen m (TypeOf expr)) => Infer m (FromNom nomId expr)

Defined in Hyper.Type.AST.Nominal

Methods

inferBody :: forall (h :: AHyperType -> Type). (FromNom nomId expr # InferChild m h) -> m (FromNom nomId expr # h, InferOf (FromNom nomId expr) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (FromNom nomId expr) -> Dict (HNodesConstraint (FromNom nomId expr) (Infer m), HNodesConstraint (InferOf (FromNom nomId expr)) (UnifyGen m))

(MonadScopeLevel m, MonadNominals nomId (TypeOf expr) m, HTraversable (NomVarTypes (TypeOf expr)), HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m), UnifyGen m (TypeOf expr), HasInferredType expr, Infer m expr) => Infer m (ToNom nomId expr)

Defined in Hyper.Type.AST.Nominal

Methods

inferBody :: forall (h :: AHyperType -> Type). (ToNom nomId expr # InferChild m h) -> m (ToNom nomId expr # h, InferOf (ToNom nomId expr) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (ToNom nomId expr) -> Dict (HNodesConstraint (ToNom nomId expr) (Infer m), HNodesConstraint (InferOf (ToNom nomId expr)) (UnifyGen m))

(MonadScopeLevel m, LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m, UnifyGen m (TypeOf expr), HasInferredType expr, HNodesConstraint (InferOf expr) (UnifyGen m), HTraversable (InferOf expr), Infer m expr) => Infer m (Let v expr)

Defined in Hyper.Type.AST.Let

Methods

inferBody :: forall (h :: AHyperType -> Type). (Let v expr # InferChild m h) -> m (Let v expr # h, InferOf (Let v expr) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (Let v expr) -> Dict (HNodesConstraint (Let v expr) (Infer m), HNodesConstraint (InferOf (Let v expr)) (UnifyGen m))

(Infer m t, UnifyGen m (TypeOf t), HSubset' (TypeOf t) (FuncType (TypeOf t)), HasInferredType t, LocalScopeType v (UVarOf m # TypeOf t) m) => Infer m (Lam v t)

Defined in Hyper.Type.AST.Lam

Methods

inferBody :: forall (h :: AHyperType -> Type). (Lam v t # InferChild m h) -> m (Lam v t # h, InferOf (Lam v t) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (Lam v t) -> Dict (HNodesConstraint (Lam v t) (Infer m), HNodesConstraint (InferOf (Lam v t)) (UnifyGen m))

(InferOf a ~ InferOf b, Infer m a, Infer m b) => Infer m (a :+: b)

Defined in Hyper.Class.Infer

Methods

inferBody :: forall (h :: AHyperType -> Type). ((a :+: b) # InferChild m h) -> m ((a :+: b) # h, InferOf (a :+: b) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (a :+: b) -> Dict (HNodesConstraint (a :+: b) (Infer m), HNodesConstraint (InferOf (a :+: b)) (UnifyGen m))

(Infer m t, Infer m e, HasInferredType e, UnifyGen m (TypeOf e), HSubset' (TypeOf e) (FuncType (TypeOf e)), HNodeLens (InferOf t) (TypeOf e), LocalScopeType v (UVarOf m # TypeOf e) m) => Infer m (TypedLam v t e)

Defined in Hyper.Type.AST.TypedLam

Methods

inferBody :: forall (h :: AHyperType -> Type). (TypedLam v t e # InferChild m h) -> m (TypedLam v t e # h, InferOf (TypedLam v t e) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (TypedLam v t e) -> Dict (HNodesConstraint (TypedLam v t e) (Infer m), HNodesConstraint (InferOf (TypedLam v t e)) (UnifyGen m))

Infer m h => Infer m (M1 i c h)

Defined in Hyper.Class.Infer

Methods

inferBody :: forall (h0 :: AHyperType -> Type). (M1 i c h # InferChild m h0) -> m (M1 i c h # h0, InferOf (M1 i c h) # UVarOf m)

inferContext :: proxy0 m -> proxy1 (M1 i c h) -> Dict (HNodesConstraint (M1 i c h) (Infer m), HNodesConstraint (InferOf (M1 i c h)) (UnifyGen m))

Recursive (Infer m)

Defined in Hyper.Class.Infer

Methods

recurse :: forall (h :: HyperType) proxy. (HNodes h, Infer m h) => proxy (Infer m h) -> Dict (HNodesConstraint h (Infer m))

newtype InferChild m h t

A HyperType containing an inference action.

The caller may modify the scope before invoking the action via localScopeType or localLevel

Constructors

InferChild

Fields

• inferChild :: m (InferredChild (UVarOf m) h t)

_InferChild :: forall m h t m h t. Iso (InferChild m h t) (InferChild m h t) (m (InferredChild (UVarOf m) h t)) (m (InferredChild (UVarOf m) h t))

data InferredChild v h t

A HyperType containing an inferred child node

Constructors

InferredChild

Fields

• _inRep :: !(h t)

  Inferred node.

  An inferBody implementation needs to place this value in the corresponding child node of the inferred term body

• _inType :: !(InferOf (GetHyperType t) # v)

  The inference result for the child node.

  An inferBody implementation may use it to perform unifications with it.

inType :: forall v h t v. Lens (InferredChild v h t) (InferredChild v h t) ((#) (InferOf (GetHyperType t)) v) ((#) (InferOf (GetHyperType t)) v)

inRep :: forall v h t h. Lens (InferredChild v h t) (InferredChild v h t) (h t) (h t)