Disco.Typecheck.Util

Definition of type contexts, type errors, and various utilities used during type checking.

Documentation

type TyCtx = Ctx Term PolyType

A typing context is a mapping from term names to types.

data LocTCError

A typechecking error, wrapped up together with the name of the thing that was being checked when the error occurred.

Constructors

LocTCError (Maybe (QName Term)) TCError

Instances

Show LocTCError

Defined in Disco.Typecheck.Util

Methods

showsPrec :: Int -> LocTCError -> ShowS

show :: LocTCError -> String

showList :: [LocTCError] -> ShowS

noLoc :: TCError -> LocTCError

Wrap a TCError into a LocTCError with no explicit provenance information.

data TCError

Potential typechecking errors.

Constructors

Unbound (Name Term)

Encountered an unbound variable

Ambiguous (Name Term) [ModuleName]

Encountered an ambiguous name.

NoType (Name Term)

No type is specified for a definition

NotCon Con Term Type

The type of the term should have an outermost constructor matching Con, but it has type Type instead

EmptyCase

Case analyses cannot be empty.

PatternType Con Pattern Type

The given pattern should have the type, but it doesn't. instead it has a kind of type given by the Con.

DuplicateDecls (Name Term)

Duplicate declarations.

DuplicateDefns (Name Term)

Duplicate definitions.

DuplicateTyDefns String

Duplicate type definitions.

CyclicTyDef String

Cyclic type definition.

NumPatterns

# of patterns does not match type in definition

NoSearch Type

Type can't be quantified over.

Unsolvable SolveError

The constraint solver couldn't find a solution.

NotTyDef String

An undefined type name was used.

NoTWild

Wildcards are not allowed in terms.

NotEnoughArgs Con

Not enough arguments provided to type constructor.

TooManyArgs Con

Too many arguments provided to type constructor.

UnboundTyVar (Name Type)

Unbound type variable

NoPolyRec String [String] [Type]

Polymorphic recursion is not allowed

NoError

Not an error. The identity of the Monoid TCError instance.

Instances

Show TCError

Defined in Disco.Typecheck.Util

Methods

showsPrec :: Int -> TCError -> ShowS

show :: TCError -> String

showList :: [TCError] -> ShowS

Semigroup TCError

Defined in Disco.Typecheck.Util

Methods

(<>) :: TCError -> TCError -> TCError

sconcat :: NonEmpty TCError -> TCError

stimes :: Integral b => b -> TCError -> TCError

Monoid TCError

TCError is a monoid where we simply discard the first error.

Defined in Disco.Typecheck.Util

Methods

mempty :: TCError

mappend :: TCError -> TCError -> TCError

mconcat :: [TCError] -> TCError

constraint :: Member (Writer Constraint) r => Constraint -> Sem r ()

Emit a constraint.

constraints :: Member (Writer Constraint) r => [Constraint] -> Sem r ()

Emit a list of constraints.

forAll :: Member (Writer Constraint) r => [Name Type] -> Sem r a -> Sem r a

Close over the current constraint with a forall.

cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()

Run two constraint-generating actions and combine the constraints via disjunction.

withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint)

Run a computation that generates constraints, returning the generated Constraint along with the output. Note that this locally dispatches the constraint writer effect.

This function is somewhat low-level; typically you should use solve instead, which also solves the generated constraints.

solve :: Members '[Reader TyDefCtx, Error TCError, Output Message] r => Sem (Writer Constraint ': r) a -> Sem r (a, S)

Run a computation and solve its generated constraint, returning the resulting substitution (or failing with an error). Note that this locally dispatches the constraint writer effect.

lookupTyDefn :: Members '[Reader TyDefCtx, Error TCError] r => String -> [Type] -> Sem r Type

Look up the definition of a named type. Throw a NotTyDef error if it is not found.

withTyDefns :: Member (Reader TyDefCtx) r => TyDefCtx -> Sem r a -> Sem r a

Run a subcomputation with an extended type definition context.

freshTy :: Member Fresh r => Sem r Type

Generate a type variable with a fresh name.

freshAtom :: Member Fresh r => Sem r Atom

Generate a fresh variable as an atom.