| Copyright | (c) 2016 disco team (see LICENSE) |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Disco.Typecheck.Util
Description
Definition of type contexts, type errors, and various utilities used during type checking.
Synopsis
- type TyCtx = Ctx Term PolyType
- data LocTCError = LocTCError (Maybe (QName Term)) TCError
- noLoc :: TCError -> LocTCError
- data TCError
- = Unbound (Name Term)
- | Ambiguous (Name Term) [ModuleName]
- | NoType (Name Term)
- | NotCon Con Term Type
- | EmptyCase
- | PatternType Con Pattern Type
- | DuplicateDecls (Name Term)
- | DuplicateDefns (Name Term)
- | DuplicateTyDefns String
- | CyclicTyDef String
- | NumPatterns
- | NonlinearPattern Pattern (Name Term)
- | NoSearch Type
- | Unsolvable SolveError
- | NotTyDef String
- | NoTWild
- | NotEnoughArgs Con
- | TooManyArgs Con
- | UnboundTyVar (Name Type)
- | NoPolyRec String [String] [Type]
- | NoError
- constraint :: Member (Writer Constraint) r => Constraint -> Sem r ()
- constraints :: Member (Writer Constraint) r => [Constraint] -> Sem r ()
- forAll :: Member (Writer Constraint) r => [Name Type] -> Sem r a -> Sem r a
- cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()
- withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint)
- solve :: Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r => Sem (Writer Constraint ': r) a -> Sem r (a, S)
- lookupTyDefn :: Members '[Reader TyDefCtx, Error TCError] r => String -> [Type] -> Sem r Type
- withTyDefns :: Member (Reader TyDefCtx) r => TyDefCtx -> Sem r a -> Sem r a
- freshTy :: Member Fresh r => Sem r Type
- freshAtom :: Member Fresh r => Sem r Atom
Documentation
data LocTCError Source #
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 Source # | |
Defined in Disco.Typecheck.Util Methods showsPrec :: Int -> LocTCError -> ShowS # show :: LocTCError -> String # showList :: [LocTCError] -> ShowS # | |
noLoc :: TCError -> LocTCError Source #
Wrap a TCError into a LocTCError with no explicit provenance
information.
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 |
| 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 |
| NonlinearPattern Pattern (Name Term) | Duplicate variable in a pattern |
| 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
|
constraint :: Member (Writer Constraint) r => Constraint -> Sem r () Source #
Emit a constraint.
constraints :: Member (Writer Constraint) r => [Constraint] -> Sem r () Source #
Emit a list of constraints.
forAll :: Member (Writer Constraint) r => [Name Type] -> Sem r a -> Sem r a Source #
Close over the current constraint with a forall.
cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r () Source #
Run two constraint-generating actions and combine the constraints via disjunction.
withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint) Source #
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 ann)] r => Sem (Writer Constraint ': r) a -> Sem r (a, S) Source #
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 Source #
Look up the definition of a named type. Throw a NotTyDef error
if it is not found.