module Mikan.Syntax.Scope.Errors where

import Control.DeepSeq

import GHC.Generics

import Mikan.Interaction.Options.Warnings

import Mikan.Syntax.Abstract.PatternSynonyms
import Mikan.Syntax.Concrete.Definitions
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.State
import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Pretty

import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.List1 (List1, NonEmpty((:|)))

data IgnoredRecordDeclaration
  = FieldOutsideRecord
  | PrivateRecordField !KwRange C.Name
  | NotValidBeforeField NiceDeclaration
  deriving (Int -> IgnoredRecordDeclaration -> ShowS
[IgnoredRecordDeclaration] -> ShowS
IgnoredRecordDeclaration -> String
(Int -> IgnoredRecordDeclaration -> ShowS)
-> (IgnoredRecordDeclaration -> String)
-> ([IgnoredRecordDeclaration] -> ShowS)
-> Show IgnoredRecordDeclaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IgnoredRecordDeclaration -> ShowS
showsPrec :: Int -> IgnoredRecordDeclaration -> ShowS
$cshow :: IgnoredRecordDeclaration -> String
show :: IgnoredRecordDeclaration -> String
$cshowList :: [IgnoredRecordDeclaration] -> ShowS
showList :: [IgnoredRecordDeclaration] -> ShowS
Show, (forall x.
 IgnoredRecordDeclaration -> Rep IgnoredRecordDeclaration x)
-> (forall x.
    Rep IgnoredRecordDeclaration x -> IgnoredRecordDeclaration)
-> Generic IgnoredRecordDeclaration
forall x.
Rep IgnoredRecordDeclaration x -> IgnoredRecordDeclaration
forall x.
IgnoredRecordDeclaration -> Rep IgnoredRecordDeclaration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x.
IgnoredRecordDeclaration -> Rep IgnoredRecordDeclaration x
from :: forall x.
IgnoredRecordDeclaration -> Rep IgnoredRecordDeclaration x
$cto :: forall x.
Rep IgnoredRecordDeclaration x -> IgnoredRecordDeclaration
to :: forall x.
Rep IgnoredRecordDeclaration x -> IgnoredRecordDeclaration
Generic)

instance PrettyTCM IgnoredRecordDeclaration where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
IgnoredRecordDeclaration -> m Doc
prettyTCM = \case
    IgnoredRecordDeclaration
FieldOutsideRecord -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"This" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"field"]
       [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"declaration cannot appear outside a"
       [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"record", m Doc
"declaration. It will be ignored."]
    PrivateRecordField KwRange
_ Name
nm -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"This" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"private"]
       [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"block has no effect on the record field" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
nm m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    NotValidBeforeField NiceDeclaration
nd -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
       ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"This declaration can not appear before the last"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"field", m Doc
"of", m Doc
"a", m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"record"]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"declaration. It will be ignored."

instance NFData IgnoredRecordDeclaration

instance Diagnostic IgnoredRecordDeclaration where
  diagnosticReason :: IgnoredRecordDeclaration -> DiagnosticReason
diagnosticReason = \case
    NotValidBeforeField{} -> DiagnosticReason
DiagError
    FieldOutsideRecord{}  -> DiagnosticReason
DiagError
    PrivateRecordField{}  -> WarningName -> DiagnosticReason
DiagWarning WarningName
UselessPrivate_

  diagnosticString :: IgnoredRecordDeclaration -> String
diagnosticString = \case
    NotValidBeforeField{} -> String
"NotValidBeforeField"
    FieldOutsideRecord{}  -> String
"FieldOutsideRecord"
    PrivateRecordField{}  -> String
"UselessPrivate"

-- Pattern synonym errors
data PatternSynonymError
  = AsPatternInPatternSynonym
  | DotPatternInPatternSynonym
  | BadArgumentsToPatternSynonym A.AmbiguousQName
  | TooFewArgumentsToPatternSynonym A.AmbiguousQName
  | CannotResolveAmbiguousPatternSynonym (List1 (A.QName, A.PatternSynDefn))
  | IllegalInstanceVariableInPatternSynonym C.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 C.Name (List1 A.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 C.Name
    -- ^ This variable is only bound on the lhs of the pattern synonym, not on the rhs.
  | WildcardInPatternSynonym C.Name
    -- ^ The given name is a 'simpleHole' on the lhs of a pattern synonym.
  | UnboundVariablesInPatternSynonym (List1 A.Name)
    -- ^ These variables are only bound on the rhs of the pattern synonym, not on the lhs.
  deriving (Int -> PatternSynonymError -> ShowS
[PatternSynonymError] -> ShowS
PatternSynonymError -> String
(Int -> PatternSynonymError -> ShowS)
-> (PatternSynonymError -> String)
-> ([PatternSynonymError] -> ShowS)
-> Show PatternSynonymError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PatternSynonymError -> ShowS
showsPrec :: Int -> PatternSynonymError -> ShowS
$cshow :: PatternSynonymError -> String
show :: PatternSynonymError -> String
$cshowList :: [PatternSynonymError] -> ShowS
showList :: [PatternSynonymError] -> ShowS
Show, (forall x. PatternSynonymError -> Rep PatternSynonymError x)
-> (forall x. Rep PatternSynonymError x -> PatternSynonymError)
-> Generic PatternSynonymError
forall x. Rep PatternSynonymError x -> PatternSynonymError
forall x. PatternSynonymError -> Rep PatternSynonymError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PatternSynonymError -> Rep PatternSynonymError x
from :: forall x. PatternSynonymError -> Rep PatternSynonymError x
$cto :: forall x. Rep PatternSynonymError x -> PatternSynonymError
to :: forall x. Rep PatternSynonymError x -> PatternSynonymError
Generic)

instance NFData PatternSynonymError

instance PrettyTCM PatternSynonymError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => PatternSynonymError -> m Doc
prettyTCM = \case
    PatternSynonymError
AsPatternInPatternSynonym -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"@-patterns are not allowed in pattern synonyms"

    PatternSynonymError
DotPatternInPatternSynonym -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords
      String
"Dot or equality patterns are not allowed in pattern synonyms. Maybe use '_' instead."

    BadArgumentsToPatternSynonym AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Bad arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
A.headAmbQ AmbiguousQName
x]

    TooFewArgumentsToPatternSynonym AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Too few arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
A.headAmbQ AmbiguousQName
x]

    CannotResolveAmbiguousPatternSynonym List1 (QName, PatternSynDefn)
defs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot resolve overloaded pattern synonym" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
               String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"since candidates have different shapes:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ ((QName, PatternSynDefn) -> m Doc)
-> List1 (QName, PatternSynDefn) -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName, PatternSynDefn) -> m Doc
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
(QName, PatternSynDefn) -> m Doc
prDef List1 (QName, PatternSynDefn)
defs
      , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(hint: overloaded pattern synonyms must be equal up to variable and constructor names)"
      ]
      where
        (QName
x, PatternSynDefn
_) = List1 (QName, PatternSynDefn) -> (QName, PatternSynDefn)
forall a. NonEmpty a -> a
List1.head List1 (QName, PatternSynDefn)
defs
        prDef :: (QName, PatternSynDefn) -> m Doc
prDef (QName
x, (A.PatternSynDefn [WithHiding Name]
xs Pattern' Void
p)) = Declaration -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (QName -> [WithHiding BindName] -> Pattern' Void -> Declaration
A.PatternSynDef QName
x ((WithHiding Name -> WithHiding BindName)
-> [WithHiding Name] -> [WithHiding BindName]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> BindName) -> WithHiding Name -> WithHiding BindName
forall a b. (a -> b) -> WithHiding a -> WithHiding b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
A.BindName) [WithHiding Name]
xs) Pattern' Void
p) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Range
r)
          where r :: Range
r = QName -> Range
forall a. HasNameBindingSite a => a -> Range
A.nameBindingSite QName
x

    IllegalInstanceVariableInPatternSynonym Name
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Variable is bound as instance in pattern synonym,"
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but does not resolve as instance in pattern: "
      , [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x]
      ]

    PatternSynonymArgumentShadows ConstructorOrPatternSynonym
kind Name
x (AbstractName
y :| [AbstractName]
_ys) -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Pattern synonym variable"
        , [ Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x ]
        , [ m Doc
"shadows" ]
        , [ ConstructorOrPatternSynonym -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ConstructorOrPatternSynonym
kind ]
        , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"defined at:"
        ]
      , Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Range -> m Doc) -> Range -> m Doc
forall a b. (a -> b) -> a -> b
$ AbstractName -> Range
forall a. HasNameBindingSite a => a -> Range
A.nameBindingSite AbstractName
y
      ]

    UnusedVariableInPatternSynonym Name
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unused variable in pattern synonym: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x]

    WildcardInPatternSynonym Name
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Wildcard pattern in pattern synonym left-hand side: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x]

    UnboundVariablesInPatternSynonym List1 Name
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unbound variables in pattern synonym: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Name -> m Doc) -> List1 Name -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 Name
xs)]

instance Diagnostic PatternSynonymError where
  diagnosticReason :: PatternSynonymError -> DiagnosticReason
diagnosticReason PatternSynonymError
_ = DiagnosticReason
DiagError
  diagnosticString :: PatternSynonymError -> String
diagnosticString = \case
    AsPatternInPatternSynonym{}               -> String
"AsPatternInPatternSynonym"
    BadArgumentsToPatternSynonym{}            -> String
"BadArgumentsToPatternSynonym"
    CannotResolveAmbiguousPatternSynonym{}    -> String
"CannotResolveAmbiguousPatternSynonym"
    DotPatternInPatternSynonym{}              -> String
"DotPatternInPatternSynonym"
    IllegalInstanceVariableInPatternSynonym{} -> String
"IllegalInstanceVariableInPatternSynonym"
    TooFewArgumentsToPatternSynonym{}         -> String
"TooFewArgumentsToPatternSynonym"
    UnboundVariablesInPatternSynonym{}        -> String
"UnboundVariablesInPatternSynonym"
    UnusedVariableInPatternSynonym{}          -> String
"UnusedVariableInPatternSynonym"
    WildcardInPatternSynonym{}                -> String
"WildcardInPatternSynonym"
    PatternSynonymArgumentShadows ConstructorOrPatternSynonym
c Name
_ List1 AbstractName
_       -> case ConstructorOrPatternSynonym
c of
      ConstructorOrPatternSynonym
IsConstructor    -> String
"PatternSynonymArgumentShadows.Constructor"
      ConstructorOrPatternSynonym
IsPatternSynonym -> String
"PatternSynonymArgumentShadows.PatternSynonym"

lookupPatternSyn :: A.AmbiguousQName -> TCM A.PatternSynDefn
lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn AmbiguousQName
ambX = do
  let xs :: List1 QName
xs = AmbiguousQName -> List1 QName
A.getAmbiguous AmbiguousQName
ambX
  defs <- (QName -> TCM PatternSynDefn)
-> List1 QName -> TCMT IO (NonEmpty PatternSynDefn)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse QName -> TCM PatternSynDefn
lookupSinglePatternSyn List1 QName
xs
  case mergePatternSynDefs defs of
    Just PatternSynDefn
def   -> PatternSynDefn -> TCM PatternSynDefn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
def
    Maybe PatternSynDefn
Nothing    -> PatternSynonymError -> TCM PatternSynDefn
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (PatternSynonymError -> TCM PatternSynDefn)
-> PatternSynonymError -> TCM PatternSynDefn
forall a b. (a -> b) -> a -> b
$ List1 (QName, PatternSynDefn) -> PatternSynonymError
CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn) -> PatternSynonymError)
-> List1 (QName, PatternSynDefn) -> PatternSynonymError
forall a b. (a -> b) -> a -> b
$ List1 QName
-> NonEmpty PatternSynDefn -> List1 (QName, PatternSynDefn)
forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
List1.zip List1 QName
xs NonEmpty PatternSynDefn
defs