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

Language | Haskell98 |

- equivT :: Ord n => EnvT n -> Type n -> Type n -> Bool
- equivWithBindsT :: Ord n => EnvT n -> [Bind n] -> [Bind n] -> Type n -> Type n -> Bool
- equivTyCon :: Eq n => TyCon n -> TyCon n -> Bool
- crushHeadT :: Ord n => EnvT n -> Type n -> Type n
- crushSomeT :: Ord n => EnvT n -> Type n -> Type n
- crushEffect :: Ord n => EnvT n -> Effect n -> Effect n

# Documentation

equivT :: Ord n => EnvT n -> Type n -> Type n -> Bool Source #

Check equivalence of types.

Checks equivalence up to alpha-renaming, as well as crushing of effects and trimming of closures.

- Return
`False`

if we find any free variables. - We assume the types are well-kinded, so that the type annotations on bound variables match the binders. If this is not the case then you get an indeterminate result.

:: Ord n | |

=> EnvT n | Environment of types. |

-> [Bind n] | Stack of binders for first type. |

-> [Bind n] | Stack of binders for second type. |

-> Type n | First type to compare. |

-> Type n | Second type to compare. |

-> Bool |

Like `equivT`

but take the initial stacks of type binders.

equivTyCon :: Eq n => TyCon n -> TyCon n -> Bool Source #

Check if two `TyCons`

are equivalent.
We need to handle `TyConBound`

specially incase it's kind isn't attached,

crushSomeT :: Ord n => EnvT n -> Type n -> Type n Source #

Crush compound effects and closure terms. We check for a crushable term before calling crushT because that function will recursively crush the components. As equivT is already recursive, we don't want a doubly-recursive function that tries to re-crush the same non-crushable type over and over.