{-# OPTIONS_GHC -Wunused-imports #-}
module Mikan.TypeChecking.Coverage.Errors where

import Control.DeepSeq

import Data.Maybe

import GHC.Generics

import Mikan.Syntax.Translation.InternalToAbstract
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.Signature (typeOfConst)
import Mikan.TypeChecking.Monad.Closure
import Mikan.TypeChecking.Monad.Context
import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Pretty

import Mikan.Utils.Impossible
import Mikan.Utils.Null hiding (null)

-- | Error when splitting a pattern variable into possible constructor patterns.
data SplitError
  = 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
    { SplitError -> Maybe Blocker
cantSplitBlocker  :: Maybe Blocker -- ^ Blocking metavariable (if any)
    , SplitError -> QName
cantSplitConName  :: QName         -- ^ Constructor.
    , SplitError -> Telescope
cantSplitTel      :: Telescope     -- ^ Context for indices.
    , SplitError -> Args
cantSplitConIdx   :: Args          -- ^ Inferred indices (from type of constructor).
    , SplitError -> Args
cantSplitGivenIdx :: Args          -- ^ Expected indices (from checking pattern).
    , SplitError -> [UnificationFailure]
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 A.Pattern) Type
  | CannotEliminateWithProjection
    { cantSplitBlocker   :: Maybe Blocker
      -- ^ Blocking metavariable (if any)
    , SplitError -> Type
cantSplitType      :: Type
      -- ^ Type of the RHS where we failed to disambiguate the copattern.
    , SplitError -> WhyWrongProj
cantSplitProjWhy   :: WhyWrongProj
      -- ^ Why does this projection not eliminate the given type?
    , SplitError -> WrongProjectionName
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
  deriving (Int -> SplitError -> ShowS
[SplitError] -> ShowS
SplitError -> String
(Int -> SplitError -> ShowS)
-> (SplitError -> String)
-> ([SplitError] -> ShowS)
-> Show SplitError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitError -> ShowS
showsPrec :: Int -> SplitError -> ShowS
$cshow :: SplitError -> String
show :: SplitError -> String
$cshowList :: [SplitError] -> ShowS
showList :: [SplitError] -> ShowS
Show, (forall x. SplitError -> Rep SplitError x)
-> (forall x. Rep SplitError x -> SplitError) -> Generic SplitError
forall x. Rep SplitError x -> SplitError
forall x. SplitError -> Rep SplitError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SplitError -> Rep SplitError x
from :: forall x. SplitError -> Rep SplitError x
$cto :: forall x. Rep SplitError x -> SplitError
to :: forall x. Rep SplitError x -> SplitError
Generic)

-- | A name to be reported in a failure of projection disambiguation.
data WrongProjectionName
  = 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.
  deriving (Int -> WrongProjectionName -> ShowS
[WrongProjectionName] -> ShowS
WrongProjectionName -> String
(Int -> WrongProjectionName -> ShowS)
-> (WrongProjectionName -> String)
-> ([WrongProjectionName] -> ShowS)
-> Show WrongProjectionName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WrongProjectionName -> ShowS
showsPrec :: Int -> WrongProjectionName -> ShowS
$cshow :: WrongProjectionName -> String
show :: WrongProjectionName -> String
$cshowList :: [WrongProjectionName] -> ShowS
showList :: [WrongProjectionName] -> ShowS
Show, (forall x. WrongProjectionName -> Rep WrongProjectionName x)
-> (forall x. Rep WrongProjectionName x -> WrongProjectionName)
-> Generic WrongProjectionName
forall x. Rep WrongProjectionName x -> WrongProjectionName
forall x. WrongProjectionName -> Rep WrongProjectionName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WrongProjectionName -> Rep WrongProjectionName x
from :: forall x. WrongProjectionName -> Rep WrongProjectionName x
$cto :: forall x. Rep WrongProjectionName x -> WrongProjectionName
to :: forall x. Rep WrongProjectionName x -> WrongProjectionName
Generic)

-- | Why did projection disambiguation fail at this position?
data WhyWrongProj
  = 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.
  deriving (Int -> WhyWrongProj -> ShowS
[WhyWrongProj] -> ShowS
WhyWrongProj -> String
(Int -> WhyWrongProj -> ShowS)
-> (WhyWrongProj -> String)
-> ([WhyWrongProj] -> ShowS)
-> Show WhyWrongProj
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhyWrongProj -> ShowS
showsPrec :: Int -> WhyWrongProj -> ShowS
$cshow :: WhyWrongProj -> String
show :: WhyWrongProj -> String
$cshowList :: [WhyWrongProj] -> ShowS
showList :: [WhyWrongProj] -> ShowS
Show, (forall x. WhyWrongProj -> Rep WhyWrongProj x)
-> (forall x. Rep WhyWrongProj x -> WhyWrongProj)
-> Generic WhyWrongProj
forall x. Rep WhyWrongProj x -> WhyWrongProj
forall x. WhyWrongProj -> Rep WhyWrongProj x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhyWrongProj -> Rep WhyWrongProj x
from :: forall x. WhyWrongProj -> Rep WhyWrongProj x
$cto :: forall x. Rep WhyWrongProj x -> WhyWrongProj
to :: forall x. Rep WhyWrongProj x -> WhyWrongProj
Generic)

data UnificationFailure
  = 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
  deriving (Int -> UnificationFailure -> ShowS
[UnificationFailure] -> ShowS
UnificationFailure -> String
(Int -> UnificationFailure -> ShowS)
-> (UnificationFailure -> String)
-> ([UnificationFailure] -> ShowS)
-> Show UnificationFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnificationFailure -> ShowS
showsPrec :: Int -> UnificationFailure -> ShowS
$cshow :: UnificationFailure -> String
show :: UnificationFailure -> String
$cshowList :: [UnificationFailure] -> ShowS
showList :: [UnificationFailure] -> ShowS
Show, (forall x. UnificationFailure -> Rep UnificationFailure x)
-> (forall x. Rep UnificationFailure x -> UnificationFailure)
-> Generic UnificationFailure
forall x. Rep UnificationFailure x -> UnificationFailure
forall x. UnificationFailure -> Rep UnificationFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UnificationFailure -> Rep UnificationFailure x
from :: forall x. UnificationFailure -> Rep UnificationFailure x
$cto :: forall x. Rep UnificationFailure x -> UnificationFailure
to :: forall x. Rep UnificationFailure x -> UnificationFailure
Generic)

instance NFData WrongProjectionName
instance NFData UnificationFailure
instance NFData WhyWrongProj
instance NFData SplitError

instance PrettyTCM SplitError where
  prettyTCM :: forall m. MonadPretty m => SplitError -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitError -> m Doc
prettyTCM SplitError
err = case SplitError
err of
    NotADatatype Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [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 split on argument of non-datatype" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]

    BlockedType Blocker
b Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [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 split on argument of unresolved type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]

    CoinductiveDatatype Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [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 pattern match on the coinductive type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]

    UnificationStuck Maybe Blocker
b QName
c Telescope
tel Args
cIxs Args
gIxs [UnificationFailure]
errs
      | Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
cIxs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
gIxs -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise                  -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> m Doc) -> [[m Doc]] -> m Doc
forall a b. (a -> b) -> a -> b
$
        [ [ [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]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[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
"I'm not sure if there should be a case for the constructor"
            , [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","]
            , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"because I get stuck when trying to solve the following"
            , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"unification problems (inferred index ≟ expected index):"
            ]
          ]
        , (Arg Term -> Arg Term -> m Doc) -> Args -> Args -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
prEq Args
cIxs Args
gIxs
        , if [UnificationFailure] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UnificationFailure]
errs then [] else
            ([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
"Possible", [UnificationFailure] -> m Doc -> m Doc
forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS [UnificationFailure]
errs m Doc
"reason" ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"why unification failed:")
            m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: (UnificationFailure -> m Doc) -> [UnificationFailure] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc)
-> (UnificationFailure -> m Doc) -> UnificationFailure -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnificationFailure -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnificationFailure -> m Doc
prettyTCM) [UnificationFailure]
errs
        ]
      where
        -- Andreas, 2019-08-08, issue #3943
        -- To not print hidden indices just as {_}, we strip the Arg and print
        -- the hiding information manually.
        prEq :: Arg Term -> Arg Term -> m Doc
        prEq :: Arg Term -> Arg Term -> m Doc
prEq Arg Term
cIx Arg Term
gIx = Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ 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
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ Arg Term -> m Doc
forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
 MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
 Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
cIx , m Doc
"≟" , Arg Term -> m Doc
forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
 MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
 Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
gIx ]
        pr :: Arg a -> f Doc
pr Arg a
arg = Arg a -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Arg a
arg Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM (Arg a -> a
forall e. Arg e -> e
unArg Arg a
arg)

    SplitError
CosplitNoTarget -> [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 split into projections because target type is unknown"

    CosplitNoRecordType Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \Type
t -> [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 split into projections because the target type "
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" is not a record type"

    CannotCreateMissingClause QName
f (Telescope, [NamedArg DeBruijnPattern])
cl Doc
msg Closure (Abs Type)
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot generate inferred clause for" [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
f m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Case to handle:") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [(Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope, [NamedArg DeBruijnPattern])
cl])
                                m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ ((Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
msg m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Closure (Abs Type) -> (Abs Type -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure (Abs Type)
t Abs Type -> m Doc
displayAbs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
".")
        where
        displayAbs :: Abs I.Type -> m Doc
        displayAbs :: Abs Type -> m Doc
displayAbs (Abs ArgName
x Type
t) = ArgName -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => ArgName -> m a -> m a
addContext ArgName
x (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        displayAbs (NoAbs ArgName
x Type
t) = Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
          Clause
forall a. Null a => a
empty { clauseTel = tel, namedClausePats = ps }

    SplitError
SplitOnCoinductive -> [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
"Pattern matching on coinductive types is not allowed"

    SplitOnNonVariable Term
v Type
t -> [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 pattern match because the (refined) argument " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" is not a variable."

    SplitOnNonEtaRecord QName
q -> [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 matching on no-eta record type"
      , [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q, m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc
"defined at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r) ]
      , String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not allowed"
      , [ m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
"to activate, add declaration `pattern` to record definition" ]
      ]
      where r :: Range
r = QName -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite QName
q

    SplitOnAbstract QName
d ->
      m Doc
"Cannot split on abstract data type" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d

    SplitOnUnchecked QName
d ->
      m Doc
"Cannot split on data type" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"whose definition has not yet been checked"

    SplitOnPartial Dom Type
dom -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"Splitting on partial elements is only allowed at the type Partial, but the domain here is", 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
$ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom ]

    SplitInProp DataOrRecordE
dr -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cannot split on"
      , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ DataOrRecordE -> String
kindOfData DataOrRecordE
dr
      , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in Prop unless target is in Prop"
      ]
      where
        kindOfData :: DataOrRecordE -> String
        kindOfData :: DataOrRecordE -> String
kindOfData DataOrRecordE
IsData                                                        = String
"datatype"
        kindOfData (IsRecord InductionAndEta {recordInduction :: InductionAndEta -> Maybe Induction
recordInduction=Maybe Induction
Nothing})          = String
"record type"
        kindOfData (IsRecord InductionAndEta {recordInduction :: InductionAndEta -> Maybe Induction
recordInduction=Just Induction
Inductive})   = String
"inductive record type"
        kindOfData (IsRecord InductionAndEta {recordInduction :: InductionAndEta -> Maybe Induction
recordInduction=Just Induction
CoInductive}) = String
"coinductive record type"

    SortOfSplitVarError Maybe Blocker
_ Doc
doc -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
doc

    CannotEliminateWithPattern Maybe Blocker
b NamedArg Pattern
p Type
a -> do
      let isProj :: Bool
isProj = Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isJust (NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg Pattern
p)
      [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 eliminate type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: if
         | Bool
isProj -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"with projection pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p]
         | A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
f <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"with pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(suggestion: write" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
".(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix AmbiguousQName
f) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"for a dot pattern," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"or remove the braces for a postfix projection)"
         | Bool
otherwise ->
             m Doc
"with" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Pattern -> String
forall {e}. Pattern' e -> String
kindOfPattern (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p)) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: m Doc
"pattern" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
             String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"(did you supply too many arguments?)"
      where
      kindOfPattern :: Pattern' e -> String
kindOfPattern = \case
        A.VarP{}    -> String
"variable"
        A.ConP{}    -> String
"constructor"
        A.ProjP{}   -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
        A.DefP{}    -> String
forall a. HasCallStack => a
__IMPOSSIBLE__
        A.WildP{}   -> String
"wildcard"
        A.DotP{}    -> String
"dot"
        A.AbsurdP{} -> String
"absurd"
        A.LitP{}    -> String
"literal"
        A.RecP{}    -> String
"record"
        A.WithP{}   -> String
"with"
        A.EqualP{}  -> String
"equality"
        A.AsP PatInfo
_ BindName
_ Pattern' e
p -> Pattern' e -> String
kindOfPattern Pattern' e
p
        A.PatternSynP{} -> String
forall a. HasCallStack => a
__IMPOSSIBLE__

    CannotEliminateWithProjection Maybe Blocker
_ Type
ty (BecauseAlreadyApplied Type
pty) WrongProjectionName
proj -> [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 eliminate record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty] [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
"with copattern"
      , 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
$ WrongProjectionName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM WrongProjectionName
proj m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
forall (m :: * -> *). Applicative m => m Doc
colon m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
pty
      , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"which is not in scope as a projection, because it has already been instantiated."
      ]

    CannotEliminateWithProjection Maybe Blocker
_ Type
ty WhyWrongProj
BecauseNotProj WrongProjectionName
proj -> [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 eliminate record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty]
      [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
"with copattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [WrongProjectionName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM WrongProjectionName
proj 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. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is not a projection."

    CannotEliminateWithProjection Maybe Blocker
_ Type
ty (BecauseNotRecord Maybe Doc
hint) WrongProjectionName
proj ->
      let
        body :: m Doc
body = [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 eliminate non-record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty]
          [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
"with copattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [WrongProjectionName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM WrongProjectionName
proj m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
      in m Doc -> (Doc -> m Doc) -> Maybe Doc -> m Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Doc
body (\Doc
h -> m Doc
body m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
h) Maybe Doc
hint

    CannotEliminateWithProjection Maybe Blocker
_ Type
ty (BecauseNotField []) WrongProjectionName
proj -> [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 eliminate record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty]
      [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
"with copattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [WrongProjectionName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM WrongProjectionName
proj 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. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"since it has no fields."

    CannotEliminateWithProjection Maybe Blocker
_ Type
ty (BecauseNotField [Dom QName]
fields) WrongProjectionName
proj ->
      let
        head :: m Doc
head = [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 eliminate record type" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty]
          [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
"with copattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [WrongProjectionName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM WrongProjectionName
proj 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. Semigroup a => a -> a -> a
<> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which is not one of its fields:"
        field :: Dom QName -> m Doc
        field :: Dom QName -> m Doc
field Dom QName
n = do
          t <- QName -> m Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst (Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
n)
          nest 2 $ prettyTCM (unDom n) <+> colon <+> prettyTCM t
      in [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
headm Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:(Dom QName -> m Doc) -> [Dom QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> m Doc
field [Dom QName]
fields

    GenericSplitError String
s -> [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
"Split failed:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
s

instance PrettyTCM WrongProjectionName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => WrongProjectionName -> m Doc
prettyTCM = \case
    UnambWrongProj QName
p -> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p
    AmbWrongProj   QName
p -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
p

instance PrettyTCM UnificationFailure where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => UnificationFailure -> m Doc
prettyTCM UnificationFailure
err = case UnificationFailure
err of
    UnifyIndicesNotVars Telescope
tel Type
a Term
u Term
v Args
ixs -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [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 apply injectivity to the equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"because I cannot generalize over the indices" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
ixs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    UnifyRecursiveEq Telescope
tel Type
a Int
i Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [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 solve variable " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" of type " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" with solution " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" because the variable occurs in the solution," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
" or in the type of one of the variables in the solution."

    UnifyReflexiveEq Telescope
tel Type
a Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [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 eliminate reflexive equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"of type" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"because K has been disabled."


instance Diagnostic SplitError where
  diagnosticReason :: SplitError -> DiagnosticReason
diagnosticReason SplitError
_ = DiagnosticReason
DiagError
  diagnosticString :: SplitError -> String
diagnosticString = \case
    GenericSplitError             {} -> String
"SplitError.GenericSplitError"
    BlockedType                   {} -> String
"SplitError.BlockedType"
    CannotCreateMissingClause     {} -> String
"SplitError.CannotCreateMissingClause"
    CoinductiveDatatype           {} -> String
"SplitError.CoinductiveDatatype"
    CosplitNoRecordType           {} -> String
"SplitError.CosplitNoRecordType"
    CosplitNoTarget               {} -> String
"SplitError.CosplitNoTarget"
    NotADatatype                  {} -> String
"SplitError.NotADatatype"
    UnificationStuck              {} -> String
"SplitError.UnificationStuck"
    SplitInProp                   {} -> String
"SplitError.SplitInProp"
    SplitOnAbstract               {} -> String
"SplitError.SplitOnAbstract"
    SplitOnCoinductive            {} -> String
"SplitError.SplitOnCoinductive"
    SplitOnNonEtaRecord           {} -> String
"SplitError.SplitOnNonEtaRecord"
    SplitOnNonVariable            {} -> String
"SplitError.SplitOnNonVariable"
    SplitOnPartial                {} -> String
"SplitError.SplitOnPartial"
    SplitOnUnchecked              {} -> String
"SplitError.SplitOnUnchecked"
    SortOfSplitVarError           {} -> String
"SplitError.SortOfSplitVarError"
    CannotEliminateWithPattern    {} -> String
"SplitError.CannotEliminateWithPattern"
    CannotEliminateWithProjection {} -> String
"SplitError.CannotEliminateWithProjection"