Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- termSize :: Term -> Word
- termType :: TyConMap -> Term -> Type
- applyTypeToArgs :: Term -> TyConMap -> Type -> [Either Term Type] -> Type
- piResultTy :: HasCallStack => TyConMap -> Type -> Type -> Type
- piResultTyMaybe :: HasCallStack => TyConMap -> Type -> Type -> Maybe Type
- piResultTys :: HasCallStack => TyConMap -> Type -> [Type] -> Type
- isFun :: TyConMap -> Term -> Bool
- isPolyFun :: TyConMap -> Term -> Bool
- isLam :: Term -> Bool
- isLet :: Term -> Bool
- isVar :: Term -> Bool
- isLocalVar :: Term -> Bool
- isCon :: Term -> Bool
- isPrim :: Term -> Bool

# Documentation

applyTypeToArgs :: Term -> TyConMap -> Type -> [Either Term Type] -> Type Source #

Get the result type of a polymorphic function given a list of arguments

piResultTy :: HasCallStack => TyConMap -> Type -> Type -> Type Source #

Like `piResultTyMaybe`

, but errors out when a type application is not
valid.

Do not iterate `piResultTy`

, because it's inefficient to substitute one
variable at a time; instead use `piResultTys`

piResultTyMaybe :: HasCallStack => TyConMap -> Type -> Type -> Maybe Type Source #

Like `piResultTys`

but for a single argument.

Do not iterate `piResultTyMaybe`

, because it's inefficient to substitute one
variable at a time; instead use `piResultTys`

piResultTys :: HasCallStack => TyConMap -> Type -> [Type] -> Type Source #

`(piResultTys f_ty [ty1, ..., tyn])`

give sthe type of `(f ty1 .. tyn)`

where `f :: f_ty`

`piResultTys`

is interesting because:

`f_ty`

may have more foralls than there are args- Less obviously, it may have fewer foralls

Fore case 2. think of:

piResultTys (forall a . a) [forall b.b, Int]

This really can happen, such as situations involving `undefined`

s type:

undefined :: forall a. a

undefined (forall b. b -> b) Int

This term should have the type `(Int -> Int)`

, but notice that there are
more type args than foralls in `undefined`

s type.

For efficiency reasons, when there are no foralls, we simply drop arrows from a function type/kind.

isLocalVar :: Term -> Bool Source #