module Mikan.TypeChecking.InstanceArguments.Errors where

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.Base
import Control.DeepSeq
import Mikan.Syntax.Common
import GHC.Generics (Generic)
import Mikan.Syntax.Internal
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.TypeChecking.Pretty
import Mikan.Interaction.Options.Warnings

-- | Reason for why the instance type is invalid.
data WhyInvalidInstanceType
  = 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
  deriving (Int -> WhyInvalidInstanceType -> ShowS
[WhyInvalidInstanceType] -> ShowS
WhyInvalidInstanceType -> String
(Int -> WhyInvalidInstanceType -> ShowS)
-> (WhyInvalidInstanceType -> String)
-> ([WhyInvalidInstanceType] -> ShowS)
-> Show WhyInvalidInstanceType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhyInvalidInstanceType -> ShowS
showsPrec :: Int -> WhyInvalidInstanceType -> ShowS
$cshow :: WhyInvalidInstanceType -> String
show :: WhyInvalidInstanceType -> String
$cshowList :: [WhyInvalidInstanceType] -> ShowS
showList :: [WhyInvalidInstanceType] -> ShowS
Show, (forall x. WhyInvalidInstanceType -> Rep WhyInvalidInstanceType x)
-> (forall x.
    Rep WhyInvalidInstanceType x -> WhyInvalidInstanceType)
-> Generic WhyInvalidInstanceType
forall x. Rep WhyInvalidInstanceType x -> WhyInvalidInstanceType
forall x. WhyInvalidInstanceType -> Rep WhyInvalidInstanceType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhyInvalidInstanceType -> Rep WhyInvalidInstanceType x
from :: forall x. WhyInvalidInstanceType -> Rep WhyInvalidInstanceType x
$cto :: forall x. Rep WhyInvalidInstanceType x -> WhyInvalidInstanceType
to :: forall x. Rep WhyInvalidInstanceType x -> WhyInvalidInstanceType
Generic)

instance NFData WhyInvalidInstanceType

data InstanceSearchError
  = InstanceNoCandidate Type [(Term, TCErr)]
  -- ^ The list can be empty.
  | InstanceSearchDepthExhausted Term Type Int
  | InvalidInstanceHeadType Type WhyInvalidInstanceType
  deriving (Int -> InstanceSearchError -> ShowS
[InstanceSearchError] -> ShowS
InstanceSearchError -> String
(Int -> InstanceSearchError -> ShowS)
-> (InstanceSearchError -> String)
-> ([InstanceSearchError] -> ShowS)
-> Show InstanceSearchError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InstanceSearchError -> ShowS
showsPrec :: Int -> InstanceSearchError -> ShowS
$cshow :: InstanceSearchError -> String
show :: InstanceSearchError -> String
$cshowList :: [InstanceSearchError] -> ShowS
showList :: [InstanceSearchError] -> ShowS
Show, (forall x. InstanceSearchError -> Rep InstanceSearchError x)
-> (forall x. Rep InstanceSearchError x -> InstanceSearchError)
-> Generic InstanceSearchError
forall x. Rep InstanceSearchError x -> InstanceSearchError
forall x. InstanceSearchError -> Rep InstanceSearchError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. InstanceSearchError -> Rep InstanceSearchError x
from :: forall x. InstanceSearchError -> Rep InstanceSearchError x
$cto :: forall x. Rep InstanceSearchError x -> InstanceSearchError
to :: forall x. Rep InstanceSearchError x -> InstanceSearchError
Generic)

instance NFData InstanceSearchError

instance PrettyTCM InstanceSearchError where
  prettyTCM :: forall m. MonadPretty m => InstanceSearchError -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => InstanceSearchError -> m Doc
prettyTCM = \case
    InstanceNoCandidate Type
t [(Term, TCErr)]
errs -> [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] -> 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
"No instance 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
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"was found in scope."
      , [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
$ ((Term, TCErr) -> m Doc) -> [(Term, TCErr)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, TCErr) -> m Doc
forall {m :: * -> *} {a} {a}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
(a, a) -> m Doc
prCand [(Term, TCErr)]
errs ]
      where
        prCand :: (a, a) -> m Doc
prCand (a
term, a
err) =
          String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"-" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
term m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"was ruled out because"
                 , a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
err ]

    InstanceSearchDepthExhausted Term
c Type
a Int
d -> [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
"Instance search depth exhausted (max depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") for candidate") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
      [m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 (Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a)]

    InvalidInstanceHeadType Type
_ WhyInvalidInstanceType
why -> [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
$ case WhyInvalidInstanceType
why of
      WhyInvalidInstanceType
ImproperInstHead -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance search can only be used to find elements in a named type"
      WhyInvalidInstanceType
ImproperInstTele -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance search cannot be used to find elements in an explicit function type"


instance Diagnostic InstanceSearchError where
  diagnosticReason :: InstanceSearchError -> DiagnosticReason
diagnosticReason InstanceSearchError
_ = DiagnosticReason
DiagError
  diagnosticString :: InstanceSearchError -> String
diagnosticString = \case
    InstanceNoCandidate Type
_ [(Term, TCErr)]
_            -> String
"InstanceNoCandidate"
    InstanceSearchDepthExhausted Term
_ Type
_ Int
_ -> String
"InstanceSearchDepthExhausted"
    InvalidInstanceHeadType Type
_ WhyInvalidInstanceType
_        -> String
"InvalidInstanceHeadType"