Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.InstanceArguments.Errors

Synopsis

data WhyInvalidInstanceType
- = ImproperInstHead
- | ImproperInstTele
data InstanceSearchError

Documentation

data WhyInvalidInstanceType Source #

Reason for why the instance type is invalid.

Constructors

ImproperInstHead	The type isn't headed by a local, a definition, or a postulate (e.g. it's a universe)
ImproperInstTele	The type we're looking for has a visible argument

Instances

Instances details

NFData WhyInvalidInstanceType Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Methods

rnf :: WhyInvalidInstanceType -> () #

Generic WhyInvalidInstanceType Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Associated Types

type Rep WhyInvalidInstanceType
Instance details Defined in Mikan.TypeChecking.InstanceArguments.Errors type Rep WhyInvalidInstanceType = D1 ('MetaData "WhyInvalidInstanceType" "Mikan.TypeChecking.InstanceArguments.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ImproperInstHead" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImproperInstTele" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: WhyInvalidInstanceType -> Rep WhyInvalidInstanceType x #

to :: Rep WhyInvalidInstanceType x -> WhyInvalidInstanceType #

Show WhyInvalidInstanceType Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Methods

showsPrec :: Int -> WhyInvalidInstanceType -> ShowS #

show :: WhyInvalidInstanceType -> String #

showList :: [WhyInvalidInstanceType] -> ShowS #

type Rep WhyInvalidInstanceType Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

type Rep WhyInvalidInstanceType = D1 ('MetaData "WhyInvalidInstanceType" "Mikan.TypeChecking.InstanceArguments.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ImproperInstHead" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImproperInstTele" 'PrefixI 'False) (U1 :: Type -> Type))

data InstanceSearchError Source #

Constructors

InstanceNoCandidate Type [(Term, TCErr)]	The list can be empty.
InstanceSearchDepthExhausted Term Type Int
InvalidInstanceHeadType Type WhyInvalidInstanceType

Instances

Instances details

Diagnostic InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

PrettyTCM InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Methods

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

NFData InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Methods

rnf :: InstanceSearchError -> () #

Generic InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Associated Types

type Rep InstanceSearchError

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

type Rep InstanceSearchError = D1 ('MetaData "InstanceSearchError" "Mikan.TypeChecking.InstanceArguments.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "InstanceNoCandidate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term, TCErr)])) :+: (C1 ('MetaCons "InstanceSearchDepthExhausted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: C1 ('MetaCons "InvalidInstanceHeadType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInvalidInstanceType))))

Methods

from :: InstanceSearchError -> Rep InstanceSearchError x #

to :: Rep InstanceSearchError x -> InstanceSearchError #

Show InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

Methods

showsPrec :: Int -> InstanceSearchError -> ShowS #

show :: InstanceSearchError -> String #

showList :: [InstanceSearchError] -> ShowS #

type Rep InstanceSearchError Source #

Instance details

Defined in Mikan.TypeChecking.InstanceArguments.Errors

type Rep InstanceSearchError = D1 ('MetaData "InstanceSearchError" "Mikan.TypeChecking.InstanceArguments.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "InstanceNoCandidate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term, TCErr)])) :+: (C1 ('MetaCons "InstanceSearchDepthExhausted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: C1 ('MetaCons "InvalidInstanceHeadType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInvalidInstanceType))))