ddc-core-0.4.1.3: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe-Inferred

DDC.Type.Equiv

Synopsis

Documentation

equivT :: Ord n => Type n -> Type n -> BoolSource

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.

equivWithBindsT :: Ord n => [Bind n] -> [Bind n] -> Type n -> Type n -> BoolSource

Like equivT but take the initial stacks of type binders.

equivTyCon :: Eq n => TyCon n -> TyCon n -> BoolSource

Check if two TyCons are equivalent. We need to handle TyConBound specially incase it's kind isn't attached,