Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.Syntax.Scope.Errors

Documentation

data IgnoredRecordDeclaration Source #

Constructors

FieldOutsideRecord
PrivateRecordField !KwRange Name
NotValidBeforeField NiceDeclaration

Instances

Instances details

Diagnostic IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

PrettyTCM IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

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

NFData IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

rnf :: IgnoredRecordDeclaration -> () #

Generic IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Associated Types

type Rep IgnoredRecordDeclaration

Instance details

Defined in Mikan.Syntax.Scope.Errors

type Rep IgnoredRecordDeclaration = D1 ('MetaData "IgnoredRecordDeclaration" "Mikan.Syntax.Scope.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FieldOutsideRecord" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrivateRecordField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "NotValidBeforeField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration))))

Methods

from :: IgnoredRecordDeclaration -> Rep IgnoredRecordDeclaration x #

to :: Rep IgnoredRecordDeclaration x -> IgnoredRecordDeclaration #

Show IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

showsPrec :: Int -> IgnoredRecordDeclaration -> ShowS #

show :: IgnoredRecordDeclaration -> String #

showList :: [IgnoredRecordDeclaration] -> ShowS #

type Rep IgnoredRecordDeclaration Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

type Rep IgnoredRecordDeclaration = D1 ('MetaData "IgnoredRecordDeclaration" "Mikan.Syntax.Scope.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "FieldOutsideRecord" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrivateRecordField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "NotValidBeforeField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NiceDeclaration))))

data PatternSynonymError Source #

Constructors

AsPatternInPatternSynonym
DotPatternInPatternSynonym
BadArgumentsToPatternSynonym AmbiguousQName
TooFewArgumentsToPatternSynonym AmbiguousQName
CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn))
IllegalInstanceVariableInPatternSynonym Name	This variable is bound in the lhs of the pattern synonym in instance position, but not on the rhs. This is forbidden because expansion of pattern synonyms would not be faithful to availability of instances in instance search.
PatternSynonymArgumentShadows ConstructorOrPatternSynonym Name (List1 AbstractName)	A variable to be bound in the pattern synonym resolved on the rhs as name of a constructor or a pattern synonym. The resolvents are given in the list.
UnusedVariableInPatternSynonym Name	This variable is only bound on the lhs of the pattern synonym, not on the rhs.
WildcardInPatternSynonym Name	The given name is a `simpleHole` on the lhs of a pattern synonym.
UnboundVariablesInPatternSynonym (List1 Name)	These variables are only bound on the rhs of the pattern synonym, not on the lhs.

Instances

Instances details

Diagnostic PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

PrettyTCM PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

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

NFData PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

rnf :: PatternSynonymError -> () #

Generic PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Associated Types

type Rep PatternSynonymError

Instance details

Defined in Mikan.Syntax.Scope.Errors

type Rep PatternSynonymError = D1 ('MetaData "PatternSynonymError" "Mikan.Syntax.Scope.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (((C1 ('MetaCons "AsPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BadArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "TooFewArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (QName, PatternSynDefn))))))) :+: ((C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatternSynonymArgumentShadows" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))))) :+: (C1 ('MetaCons "UnusedVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "WildcardInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "UnboundVariablesInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name)))))))

Methods

from :: PatternSynonymError -> Rep PatternSynonymError x #

to :: Rep PatternSynonymError x -> PatternSynonymError #

Show PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

Methods

showsPrec :: Int -> PatternSynonymError -> ShowS #

show :: PatternSynonymError -> String #

showList :: [PatternSynonymError] -> ShowS #

type Rep PatternSynonymError Source #

Instance details

Defined in Mikan.Syntax.Scope.Errors

type Rep PatternSynonymError = D1 ('MetaData "PatternSynonymError" "Mikan.Syntax.Scope.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (((C1 ('MetaCons "AsPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DotPatternInPatternSynonym" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BadArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "TooFewArgumentsToPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (QName, PatternSynDefn))))))) :+: ((C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatternSynonymArgumentShadows" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))))) :+: (C1 ('MetaCons "UnusedVariableInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "WildcardInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "UnboundVariablesInPatternSynonym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Name)))))))

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn Source #