Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Coverage.Errors

Synopsis

data SplitError
- = NotADatatype (Closure Type)
- | BlockedType Blocker (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck {
  - cantSplitBlocker :: Maybe Blocker
  - cantSplitConName :: QName
  - cantSplitTel :: Telescope
  - cantSplitConIdx :: Args
  - cantSplitGivenIdx :: Args
  - cantSplitFailures :: [UnificationFailure]
  }
- | CosplitNoTarget
- | CosplitNoRecordType (Closure Type)
- | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
- | CannotEliminateWithPattern (Maybe Blocker) (NamedArg Pattern) Type
- | CannotEliminateWithProjection {
  - cantSplitBlocker :: Maybe Blocker
  - cantSplitType :: Type
  - cantSplitProjWhy :: WhyWrongProj
  - cantSplitProjName :: WrongProjectionName
  }
- | SortOfSplitVarError (Maybe Blocker) Doc
- | SplitOnCoinductive
- | SplitOnNonVariable Term Type
- | SplitOnNonEtaRecord QName
- | SplitOnAbstract QName
- | SplitOnUnchecked QName
- | SplitOnPartial (Dom Type)
- | SplitInProp DataOrRecordE
- | GenericSplitError String
data WrongProjectionName
- = UnambWrongProj !QName
- | AmbWrongProj !QName
data WhyWrongProj
- = BecauseNotRecord (Maybe Doc)
- | BecauseNotProj
- | BecauseAlreadyApplied Type
- | BecauseNotField [Dom QName]
data UnificationFailure
- = UnifyIndicesNotVars Telescope Type Term Term Args
- | UnifyRecursiveEq Telescope Type Int Term
- | UnifyReflexiveEq Telescope Type Term

Documentation

data SplitError Source #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)	Neither data type nor record.
BlockedType Blocker (Closure Type)	Type could not be sufficiently reduced.
CoinductiveDatatype (Closure Type)	Split on codata not allowed. UNUSED, but keep! -- \| NoRecordConstructor Type -- ^ record type, but no constructor
UnificationStuck
Fields cantSplitBlocker :: Maybe Blocker Blocking metavariable (if any) cantSplitConName :: QName Constructor. cantSplitTel :: Telescope Context for indices. cantSplitConIdx :: Args Inferred indices (from type of constructor). cantSplitGivenIdx :: Args Expected indices (from checking pattern). cantSplitFailures :: [UnificationFailure] Reason(s) why unification got stuck.
CosplitNoTarget	We do not know the target type of the clause.
CosplitNoRecordType (Closure Type)	Target type is not a record type.
CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
CannotEliminateWithPattern (Maybe Blocker) (NamedArg Pattern) Type
CannotEliminateWithProjection
Fields cantSplitBlocker :: Maybe Blocker Blocking metavariable (if any) cantSplitType :: Type Type of the RHS where we failed to disambiguate the copattern. cantSplitProjWhy :: WhyWrongProj Why does this projection not eliminate the given type? cantSplitProjName :: WrongProjectionName The name of the projection which failed.
SortOfSplitVarError (Maybe Blocker) Doc	the meta is what we might be blocked on.
SplitOnCoinductive
SplitOnNonVariable Term Type
SplitOnNonEtaRecord QName
SplitOnAbstract QName
SplitOnUnchecked QName
SplitOnPartial (Dom Type)
SplitInProp DataOrRecordE
GenericSplitError String

Instances

Instances details

Diagnostic SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

diagnosticReason :: SplitError -> DiagnosticReason Source #

diagnosticString :: SplitError -> String Source #

toSomeDiagnostic :: SplitError -> SomeDiagnostic Source #

fromSomeDiagnostic :: SomeDiagnostic -> Maybe SplitError Source #

PrettyTCM SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

prettyTCM :: MonadPretty m => SplitError -> m Doc Source #

NFData SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

rnf :: SplitError -> () #

Generic SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Associated Types

type Rep SplitError

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

from :: SplitError -> Rep SplitError x #

to :: Rep SplitError x -> SplitError #

Show SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

showsPrec :: Int -> SplitError -> ShowS #

show :: SplitError -> String #

showList :: [SplitError] -> ShowS #

type Rep SplitError Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

data WrongProjectionName Source #

A name to be reported in a failure of projection disambiguation.

Constructors

UnambWrongProj !QName	We do not know what internal name the user meant; print this name without semantics.
AmbWrongProj !QName	We know exactly what internal name was meant; print it exactly.

Instances

Instances details

PrettyTCM WrongProjectionName Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

prettyTCM :: MonadPretty m => WrongProjectionName -> m Doc Source #

NFData WrongProjectionName Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

rnf :: WrongProjectionName -> () #

Generic WrongProjectionName Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Associated Types

type Rep WrongProjectionName

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

type Rep WrongProjectionName = D1 ('MetaData "WrongProjectionName" "Mikan.TypeChecking.Coverage.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "UnambWrongProj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)) :+: C1 ('MetaCons "AmbWrongProj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)))

Methods

from :: WrongProjectionName -> Rep WrongProjectionName x #

to :: Rep WrongProjectionName x -> WrongProjectionName #

Show WrongProjectionName Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

showsPrec :: Int -> WrongProjectionName -> ShowS #

show :: WrongProjectionName -> String #

showList :: [WrongProjectionName] -> ShowS #

type Rep WrongProjectionName Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

type Rep WrongProjectionName = D1 ('MetaData "WrongProjectionName" "Mikan.TypeChecking.Coverage.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "UnambWrongProj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)) :+: C1 ('MetaCons "AmbWrongProj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)))

data WhyWrongProj Source #

Why did projection disambiguation fail at this position?

Constructors

BecauseNotRecord (Maybe Doc)	The type is not a record type. The `Maybe Doc` gives a hint as for the reason.
BecauseNotProj	Because the name is not a (proper) projection.
BecauseAlreadyApplied Type	Because even though the name is a copy of a proper projection, it has lost all of its lambdas, so it no longer has a function type. The `Type` is the instantiated type of the projection function.
BecauseNotField [Dom QName]	Because the name is not one of the fields of the record, which must be one of the given list.

Instances

Instances details

NFData WhyWrongProj Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

rnf :: WhyWrongProj -> () #

Generic WhyWrongProj Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Associated Types

type Rep WhyWrongProj

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

type Rep WhyWrongProj = D1 ('MetaData "WhyWrongProj" "Mikan.TypeChecking.Coverage.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "BecauseNotRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Doc))) :+: C1 ('MetaCons "BecauseNotProj" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BecauseAlreadyApplied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "BecauseNotField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Dom QName]))))

Methods

from :: WhyWrongProj -> Rep WhyWrongProj x #

to :: Rep WhyWrongProj x -> WhyWrongProj #

Show WhyWrongProj Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

Methods

showsPrec :: Int -> WhyWrongProj -> ShowS #

show :: WhyWrongProj -> String #

showList :: [WhyWrongProj] -> ShowS #

type Rep WhyWrongProj Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.Errors

type Rep WhyWrongProj = D1 ('MetaData "WhyWrongProj" "Mikan.TypeChecking.Coverage.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "BecauseNotRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Doc))) :+: C1 ('MetaCons "BecauseNotProj" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BecauseAlreadyApplied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "BecauseNotField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Dom QName]))))

data UnificationFailure Source #

Constructors

UnifyIndicesNotVars Telescope Type Term Term Args	Failed to apply injectivity to constructor of indexed datatype
UnifyRecursiveEq Telescope Type Int Term	Can't solve equation because variable occurs in (type of) lhs
UnifyReflexiveEq Telescope Type Term	Can't solve reflexive equation because --without-K is enabled