| Copyright | (c) 2016 disco team (see LICENSE) |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | [email protected] |
| 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) [String]
- | 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) [String]
- | 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
- orElse :: 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 => Int -> Sem (Writer Constraint ': r) a -> Sem r (a, NonEmpty 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) [String] | Encountered an unbound variable. The offending variable together with some suggested in-scope names with small edit distance. |
| 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) [String] | Unbound type variable, together with suggested edits |
| 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.
orElse :: 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 => Int -> Sem (Writer Constraint ': r) a -> Sem r (a, NonEmpty S) Source #
Run a computation and solve its generated constraint, returning up to the requested number of possible resulting substitutions (or failing with an error). Note that this locally dispatches the constraint writer and solution limit effects.
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.