unison-parser-typechecker-0.0.0
Safe HaskellNone
LanguageHaskell2010

Unison.PatternMatchCoverage.Class

Synopsis

Documentation

class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc (m :: Type -> Type) | m -> vt v loc where Source #

A typeclass for the queries required to perform pattern match coverage checking.

Methods

getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc) Source #

Get the constructors of a type

getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc] Source #

Get the types of the arguments of a specific constructor

getConstructorIndexRefinements :: Type vt loc -> ConstructorReference -> m [(vt, Type vt loc)] Source #

The GADT type-index equations implied by matching the given constructor against a value of the given type — the proposition the DK indexed-types paper attaches to a constructor via the asserting type A ∧ P, recovered here by unifying the constructor's result with the scrutinee's type. Each pair maps a (rigid) index variable to the type the constructor pins it to. Empty for ordinary (non-index-pinning) constructors.

fresh :: m v Source #

Get a fresh variable

getPrettyPrintEnv :: m PrettyPrintEnv Source #

data EnumeratedConstructors vt v loc Source #

Instances

Instances details
(Show v, Show vt) => Show (EnumeratedConstructors vt v loc) Source # 
Instance details

Defined in Unison.PatternMatchCoverage.Class