Copyright | (C) 2018 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Capture-avoiding substitutions on DType
s
Documentation
Capture-avoiding substitution
unionSubsts :: DSubst -> DSubst -> Maybe DSubst Source #
Computes the union of two substitutions. Fails if both subsitutions map the same variable to different types.
Matching a type template against a type
matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst Source #
matchTy ign tmpl targ
matches a type template tmpl
against a type
target targ
. This returns a Map from names of type variables in the
type template to types if the types indeed match up, or Nothing
otherwise.
In the Just
case, it is guaranteed that every type variable mentioned
in the template is mapped by the returned substitution.
The first argument ign
tells matchTy
whether to ignore kind signatures
in the template. A kind signature in the template might mean that a type
variable has a more restrictive kind than otherwise possible, and that
mapping that type variable to a type of a different kind could be disastrous.
So, if we don't ignore kind signatures, this function returns Nothing
if
the template has a signature anywhere. If we do ignore kind signatures, it's
possible the returned map will be ill-kinded. Use at your own risk.