-- | Implementation of conversion checking errors which can reify part
-- of the context leading to the actual failure as terms.
module Agda.TypeChecking.Conversion.Errors
  (
  -- * Public interface
  -- $convErrors
    failConversion, mismatchedProjections, addConversionContext,

  -- * Unreifiable recursive calls
  -- $stackSlice
    nowConversionChecking, cutConversionErrors

  -- * Types
  , ConversionError(..)
  , ConversionZipper(..)
  , ConversionErrorContext(..)
  , FailedCompareAs(..)
  )
  where

import Control.Monad.Error.Class
import Control.Monad.Trans.Maybe
import Control.Monad.Except
import Control.Applicative
import Control.DeepSeq
import Control.Monad

import GHC.Generics (Generic)

import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Internal
import Agda.Syntax.Fixity (Precedence(TopCtx))
import Agda.Syntax.Common

import Agda.TypeChecking.Monad.Constraints
import Agda.TypeChecking.Monad.Statistics
import Agda.TypeChecking.Monad.SizedTypes
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Base

import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce

import qualified Agda.Utils.Null as Null
import Agda.Utils.Impossible
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad hiding (guard)
import Agda.Utils.Size

-- | The failing version of 'CompareAs'.
data FailedCompareAs
  = FailAsTermsOf Type Type
    -- ^ The conversion checker failed in a typed context.
    --
    -- While the conversion checker is homogeneous (so 'AsTermsOf' only
    -- stores a single type), a failing argument comparison early in the
    -- spine of a dependent function can cause the reconstructed
    -- "context" terms to be heterogeneous.
  | FailAsTypes
    -- ^ The conversion checker failed in a type-insensitive context.
  deriving (Int -> FailedCompareAs -> ShowS
[FailedCompareAs] -> ShowS
FailedCompareAs -> String
(Int -> FailedCompareAs -> ShowS)
-> (FailedCompareAs -> String)
-> ([FailedCompareAs] -> ShowS)
-> Show FailedCompareAs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FailedCompareAs -> ShowS
showsPrec :: Int -> FailedCompareAs -> ShowS
$cshow :: FailedCompareAs -> String
show :: FailedCompareAs -> String
$cshowList :: [FailedCompareAs] -> ShowS
showList :: [FailedCompareAs] -> ShowS
Show, (forall x. FailedCompareAs -> Rep FailedCompareAs x)
-> (forall x. Rep FailedCompareAs x -> FailedCompareAs)
-> Generic FailedCompareAs
forall x. Rep FailedCompareAs x -> FailedCompareAs
forall x. FailedCompareAs -> Rep FailedCompareAs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FailedCompareAs -> Rep FailedCompareAs x
from :: forall x. FailedCompareAs -> Rep FailedCompareAs x
$cto :: forall x. Rep FailedCompareAs x -> FailedCompareAs
to :: forall x. Rep FailedCompareAs x -> FailedCompareAs
Generic)

-- | A "zipper-like" representation of the edges between comparing a
-- normal form and comparing one of its immediate subterms in the
-- conversion checker's call graph.
data ConversionZipper
  -- | Thrown at the failing call.
  = ConvStop

  -- | A call to compare the body of a function-typed value.
  | ConvLam
      (Dom Type)       -- ^ Argument type
      (Abs ())         -- ^ Simplified codomain
      ArgName          -- ^ Name of the variable introduced for comparing the bodies
      ConversionZipper -- ^ Call stack suffix.

  -- | A call to compare the domain of a pair of pi types.
  | ConvDom
      (Dom ConversionZipper) -- ^ Information about the domain, and call stack suffix.
      (Abs Type)             -- ^ Codomain of the left-hand side type.
      (Abs Type)             -- ^ Codomain of the right-hand-side type.

  -- | A call to compare the codomain of a pair of pi types.
  | ConvCod
      (Dom Type)             -- ^ The domain.
      ArgName                -- ^ Name of the variable introduced for comparing the bodies
      ConversionZipper       -- ^ Call stack suffix.

  -- | A call to compare an argument to a function.
  | ConvApply
      Term                    -- ^ The head term
      (Abs Type)              -- ^ The codomain of the function type at the argument where conversion failed
      (Arg ConversionZipper)  -- ^ Information about the argument, and call stack suffix.
      [Elim]                  -- ^ Remaining arguments from the LHS term that conversion checking could not get to.
      [Elim]                  -- ^ Remaining arguments from the RHS term that conversion checking could not get to.
  deriving (Int -> ConversionZipper -> ShowS
[ConversionZipper] -> ShowS
ConversionZipper -> String
(Int -> ConversionZipper -> ShowS)
-> (ConversionZipper -> String)
-> ([ConversionZipper] -> ShowS)
-> Show ConversionZipper
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConversionZipper -> ShowS
showsPrec :: Int -> ConversionZipper -> ShowS
$cshow :: ConversionZipper -> String
show :: ConversionZipper -> String
$cshowList :: [ConversionZipper] -> ShowS
showList :: [ConversionZipper] -> ShowS
Show, (forall x. ConversionZipper -> Rep ConversionZipper x)
-> (forall x. Rep ConversionZipper x -> ConversionZipper)
-> Generic ConversionZipper
forall x. Rep ConversionZipper x -> ConversionZipper
forall x. ConversionZipper -> Rep ConversionZipper x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConversionZipper -> Rep ConversionZipper x
from :: forall x. ConversionZipper -> Rep ConversionZipper x
$cto :: forall x. Rep ConversionZipper x -> ConversionZipper
to :: forall x. Rep ConversionZipper x -> ConversionZipper
Generic)

-- | Additional information regarding why two function types are distinct.
data WhyUnequalTypes
  = forall a. (NFData a, Verbalize a) => UnequalDomain a a
    -- ^ Their domains differ in relevance/modality/etc.
  | UnequalHiding Hiding Hiding
    -- ^ Their domains differ in hiding.

-- | Additional information as for why two terms which might print the
-- same are distinct.
--
-- Some constructors are duplicated so that the explanations can be
-- printed in the correct order.
data HeadMismatch
  -- | They are distinct extended lambdas.
  = HdmExtLam   QName QName
  -- | They are distinct 'Pi' types.
  | HdmTypes    WhyUnequalTypes
  -- | They are distinct variables.
  | HdmVars     Int   Int
  -- | They are the same variable, but their spines might be
  -- interesting.
  | HdmVarSpine Int (Closure (Elims, Elims))

  | HdmVarDef -- ^ Variable-definition mismatch
  | HdmDefVar -- ^ Definition-variable mismatch
  | HdmVarCon -- ^ Variable-constructor mismatch
  | HdmConVar -- ^ Constructor-variable mismatch
  deriving (Int -> HeadMismatch -> ShowS
[HeadMismatch] -> ShowS
HeadMismatch -> String
(Int -> HeadMismatch -> ShowS)
-> (HeadMismatch -> String)
-> ([HeadMismatch] -> ShowS)
-> Show HeadMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HeadMismatch -> ShowS
showsPrec :: Int -> HeadMismatch -> ShowS
$cshow :: HeadMismatch -> String
show :: HeadMismatch -> String
$cshowList :: [HeadMismatch] -> ShowS
showList :: [HeadMismatch] -> ShowS
Show, (forall x. HeadMismatch -> Rep HeadMismatch x)
-> (forall x. Rep HeadMismatch x -> HeadMismatch)
-> Generic HeadMismatch
forall x. Rep HeadMismatch x -> HeadMismatch
forall x. HeadMismatch -> Rep HeadMismatch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HeadMismatch -> Rep HeadMismatch x
from :: forall x. HeadMismatch -> Rep HeadMismatch x
$cto :: forall x. Rep HeadMismatch x -> HeadMismatch
to :: forall x. Rep HeadMismatch x -> HeadMismatch
Generic)

-- | Whether a 'ConversionZipper' generated nontrivial wrapper terms
-- when flattening the call stack of a t'ConversionError'.
--
-- Used to print error messages with correct grammar.
data HereOrThere
  = Here  -- ^ It didn't.
  | There -- ^ It did.
  deriving (Int -> HereOrThere -> ShowS
[HereOrThere] -> ShowS
HereOrThere -> String
(Int -> HereOrThere -> ShowS)
-> (HereOrThere -> String)
-> ([HereOrThere] -> ShowS)
-> Show HereOrThere
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HereOrThere -> ShowS
showsPrec :: Int -> HereOrThere -> ShowS
$cshow :: HereOrThere -> String
show :: HereOrThere -> String
$cshowList :: [HereOrThere] -> ShowS
showList :: [HereOrThere] -> ShowS
Show, (forall x. HereOrThere -> Rep HereOrThere x)
-> (forall x. Rep HereOrThere x -> HereOrThere)
-> Generic HereOrThere
forall x. Rep HereOrThere x -> HereOrThere
forall x. HereOrThere -> Rep HereOrThere x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HereOrThere -> Rep HereOrThere x
from :: forall x. HereOrThere -> Rep HereOrThere x
$cto :: forall x. Rep HereOrThere x -> HereOrThere
to :: forall x. Rep HereOrThere x -> HereOrThere
Generic)

-- | Context for a conversion checking error.
data ConversionErrorContext
  = Floating ConversionZipper
    -- ^ It still makes sense to collect call stack information for this
    -- error.
  | Finished HereOrThere (Maybe HeadMismatch)
    -- ^ We can not, or do not want to, keep collecting call stack
    -- information for this error.
    -- Stores "crystallised" information about the actual failing
    -- comparison to use as context in error rendering.
  deriving (Int -> ConversionErrorContext -> ShowS
[ConversionErrorContext] -> ShowS
ConversionErrorContext -> String
(Int -> ConversionErrorContext -> ShowS)
-> (ConversionErrorContext -> String)
-> ([ConversionErrorContext] -> ShowS)
-> Show ConversionErrorContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConversionErrorContext -> ShowS
showsPrec :: Int -> ConversionErrorContext -> ShowS
$cshow :: ConversionErrorContext -> String
show :: ConversionErrorContext -> String
$cshowList :: [ConversionErrorContext] -> ShowS
showList :: [ConversionErrorContext] -> ShowS
Show, (forall x. ConversionErrorContext -> Rep ConversionErrorContext x)
-> (forall x.
    Rep ConversionErrorContext x -> ConversionErrorContext)
-> Generic ConversionErrorContext
forall x. Rep ConversionErrorContext x -> ConversionErrorContext
forall x. ConversionErrorContext -> Rep ConversionErrorContext x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConversionErrorContext -> Rep ConversionErrorContext x
from :: forall x. ConversionErrorContext -> Rep ConversionErrorContext x
$cto :: forall x. Rep ConversionErrorContext x -> ConversionErrorContext
to :: forall x. Rep ConversionErrorContext x -> ConversionErrorContext
Generic)

-- | A conversion checking failure.
--
-- A conversion checking error can be in two states (according to its
-- 'convErrCtx'): it is either 'Finished' or
-- 'Agda.TypeChecking.Conversion.Errors.Floating'.
--
-- A 'Finished' conversion-checking error packages a pair of unequal
-- terms, which are well-typed in the context that the error was raised
-- in, with sufficient information for printing an informative error
-- message. 'Finished' errors will not accumulate further call stack
-- information.
--
-- A 'Agda.TypeChecking.Conversion.Errors.Floating' conversion-checking
-- error is subject to be modified as the conversion checker's call
-- stack unwinds, by appending to its 'ConversionZipper'. Some frames in
-- a 'ConversionZipper' alter the context in which the terms
-- 'convErrLhs' and 'convErrRhs' should be interpreted. Floating errors
-- can be re-raised as 'Finished' errors using 'cutConversionErrors'.
-- This means that any code which catches those errors will have types
-- valid directly in the v'TypeError' closure, but no more context will
-- be accumulated for them.
data ConversionError = ConversionError
  { ConversionError -> Comparison
convErrCmp   :: Comparison
    -- ^ Were we checking for equality or subtyping?
  , ConversionError -> FailedCompareAs
convErrTys   :: FailedCompareAs
    -- ^ Were we comparing against a known type when conversion checking
    -- failed?
  , ConversionError -> Term
convErrLhs   :: Term
    -- ^ The "LHS" of the comparison (if 'CmpLeq', the subtype).
  , ConversionError -> Term
convErrRhs   :: Term
    -- ^ The "RHS" of the comparison (if 'CmpLeq', the supertype).
  , ConversionError -> ConversionErrorContext
convErrCtx   :: ConversionErrorContext
    -- ^ Call stack information about this error.
  }
  deriving (Int -> ConversionError -> ShowS
[ConversionError] -> ShowS
ConversionError -> String
(Int -> ConversionError -> ShowS)
-> (ConversionError -> String)
-> ([ConversionError] -> ShowS)
-> Show ConversionError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConversionError -> ShowS
showsPrec :: Int -> ConversionError -> ShowS
$cshow :: ConversionError -> String
show :: ConversionError -> String
$cshowList :: [ConversionError] -> ShowS
showList :: [ConversionError] -> ShowS
Show, (forall x. ConversionError -> Rep ConversionError x)
-> (forall x. Rep ConversionError x -> ConversionError)
-> Generic ConversionError
forall x. Rep ConversionError x -> ConversionError
forall x. ConversionError -> Rep ConversionError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConversionError -> Rep ConversionError x
from :: forall x. ConversionError -> Rep ConversionError x
$cto :: forall x. Rep ConversionError x -> ConversionError
to :: forall x. Rep ConversionError x -> ConversionError
Generic)

instance Show WhyUnequalTypes where
  show :: WhyUnequalTypes -> String
show = String -> WhyUnequalTypes -> String
forall a b. a -> b -> a
const String
"<WhyUnequalTypes>"

instance NFData WhyUnequalTypes where
  rnf :: WhyUnequalTypes -> ()
rnf = \case
    UnequalDomain     a
a a
b -> (a, a) -> ()
forall a. NFData a => a -> ()
rnf (a
a, a
b)
    UnequalHiding     Hiding
a Hiding
b -> (Hiding, Hiding) -> ()
forall a. NFData a => a -> ()
rnf (Hiding
a, Hiding
b)

instance NFData ConversionErrorContext
instance NFData ConversionZipper
instance NFData ConversionError
instance NFData FailedCompareAs
instance NFData HeadMismatch
instance NFData HereOrThere

-- $convErrors
--
-- Conversion checking errors are initially thrown (by 'failConversion')
-- in the /floating/ state, which means they can accumulate information
-- on where they happened as the call stack unwinds. This information
-- will be presented to the user by wrapping the actual mismatched terms
-- in a skeleton of the term where the mismatch happened. These terms
-- had better not be nonsense! This requires that recursive calls within
-- the conversion checker cooperate with the reconstruction process,
-- using the functions in this module. Their use can be summarised as
-- follows:
--
-- * A recursive call to compare a subterm of a normal form should be
--   guarded by 'addConversionContext'.
-- * A recursive call to a domain-specific conversion checking function
--   which takes the input terms apart using a nontrivial view (e.g.,
--   'Agda.TypeChecking.Conversion.equalLevel') should be guarded by
--   'nowConversionChecking'.
-- * A recursive call under an application of a nontrivial substitution
--   to the context and terms under consideration should be guarded by
--   'cutConversionErrors'.
-- * Recursive calls that preserve the definitional identities of the
--   terms under consideration do not need any special handling.
--
-- The goal of these rules is to allow for the user to pretend that
-- conversion checking works by normalising then checking for syntactic
-- equality: the reconstructed term should wrap the actual mismatch in
-- "hereditary neutrals (to the left)", i.e. everything that compared
-- equal on the way to the mismatched terms is normalised, but parts of
-- the term that are beyond the mismatch are left as-is (and, in the
-- future, will be presented "deemphasized").
--
-- /How much/ of the context to reify is a design parameter that can be
-- tuned. At the moment, we drop all 'ConvLam', 'ConvDom', 'ConvCod' and
-- __visible__ 'ConvApply' from the front of the zipper. Regardless, the
-- conversion checker must be set up as if the entire context will be
-- reified.

-- | Throw a floating t'ConversionError', given the arguments of
-- 'Agda.TypeChecking.Conversion.compareAs'.
failConversion
  :: (MonadTCError m, HasBuiltins m)
  => Comparison -- ^ Equality or subtyping?
  -> Term       -- ^ See 'convErrLhs'
  -> Term       -- ^ See 'convErrRhs'
  -> CompareAs  -- ^ Will be converted to a 'FailedCompareAs'.
  -> m a
failConversion :: forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a
failConversion Comparison
cmp Term
l Term
r CompareAs
cas = do
  as <- case CompareAs
cas of
    CompareAs
AsTypes     -> FailedCompareAs -> m FailedCompareAs
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FailedCompareAs
FailAsTypes
    AsTermsOf Type
t -> FailedCompareAs -> m FailedCompareAs
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FailedCompareAs -> m FailedCompareAs)
-> FailedCompareAs -> m FailedCompareAs
forall a b. (a -> b) -> a -> b
$ Type -> Type -> FailedCompareAs
FailAsTermsOf Type
t Type
t
    CompareAs
AsSizes     -> do
      t <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
      pure $ FailAsTermsOf t t

  typeError $ ConversionError_ ConversionError
    { convErrTys = as
    , convErrRhs = r
    , convErrLhs = l
    , convErrCmp = cmp
    , convErrCtx = Floating ConvStop
    }

-- | Add some call stack context to floating t'ConversionError's thrown
-- from the continuation.
--
-- This function should be placed on the __outside__ of 'addContext',
-- and the changes to the context should be reflected in the
-- 'ConversionZipper'.
addConversionContext
  :: (MonadTCError m, HasBuiltins m)
  => (ConversionZipper -> ConversionZipper)
    -- ^ How to modify the zipper
  -> m a
    -- ^ Generally, a recursive call to the conversion checker
  -> m a
addConversionContext :: forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
(ConversionZipper -> ConversionZipper) -> m a -> m a
addConversionContext ConversionZipper -> ConversionZipper
ext m a
cont = m a
cont m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
  TypeError CallStack
loc TCState
st cl' :: Closure TypeError
cl'@Closure{ clValue :: forall a. Closure a -> a
clValue = ConversionError_ conv :: ConversionError
conv@ConversionError{ convErrCtx :: ConversionError -> ConversionErrorContext
convErrCtx = Floating ConversionZipper
ctx } } -> do
    let
      zip :: ConversionZipper
zip   = ConversionZipper -> ConversionZipper
ext ConversionZipper
ctx
      old_c :: Maybe (Closure Call)
old_c = TCEnv -> Maybe (Closure Call)
envCall (Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
cl')
    cl <- TypeError -> m (Closure TypeError)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (TypeError -> m (Closure TypeError))
-> TypeError -> m (Closure TypeError)
forall a b. (a -> b) -> a -> b
$ ConversionError -> TypeError
ConversionError_ (ConversionError -> TypeError) -> ConversionError -> TypeError
forall a b. (a -> b) -> a -> b
$! ConversionError
conv { convErrCtx = Floating zip }
    zip `seq` old_c `seq` throwError $ TypeError loc st cl
      { clEnv = (clEnv cl) { envCall = old_c }
      }
  TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

-- $stackSlice
--
-- The 'ConversionZipper' reflects recursive calls made to conversion
-- checking of the immediate subterms of a normal form, and it can
-- handle most cases of a recursive call happening in a weakening of the
-- current context as well. However, some conversion-checking functions
-- take the input values apart in nontrivial, type-specific ways before
-- eventually calling into "ordinary" term conversion checking again.
--
-- If a floating t'ConversionError' happens in one of these eventual
-- calls, the reified call stack will not have anything corresponding to
-- the value that got taken apart; this can result in the terms
-- presented to the user being ill-typed (see
-- @test/Fail/ConvErrCtxLevels@ for an example). These calls can be
-- handled in two ways, depending on whether or not preserving the
-- surrounding context is likely to be useful in an error message. Here
-- are examples of using each:
--
-- *
--     Calls to 'Agda.TypeChecking.Conversion.equalLevel' are likely to
--     happen while checking hidden arguments to a defined symbol (e.g.
--     a universe-polymorphic data type), which is a context worth
--     preserving for error messages: telling the user @l != l'@ is
--     significantly less useful than telling them @List {l} A != List
--     {l'} B@.
--
--     Therefore, the call to 'Agda.TypeChecking.Conversion.equalLevel'
--     in 'Agda.TypeChecking.Conversion.equalTerm'' is guarded by
--     'nowConversionChecking'.  If an error happens while
--     conversion-checking some levels, the mismatched terms will be
--     /replaced/ by the (normalised forms of) the entire levels that
--     were being compared.
--
-- *
--     On the other hand, conversion checking of partial elements
--     involves nontrivial modifications to the context, and, more
--     importantly, generally happens to terms which display quite
--     terribly /before/ these substitutions are applied, often
--     involving eta-expanded extended lambdas and the primitive
--     @primPOr@. Subjectively, it's less useful to say that conversion
--     checking failed for the hard-to-read system than it is to say
--     that it failed for a particular face.
--
--     For these reasons,
--     'Agda.TypeChecking.Conversion.compareTermOnFace' (really,
--     'Agda.TypeChecking.Conversion.forallFaceMaps') uses
--     'cutConversionErrors' to turn any floating errors from
--     conversion-checking the faces into 'Finished' errors, which no
--     longer accumulate context. Whatever context was collected
--     /inside/ the face comparison will be preserved, but we will not
--     remember /that/ (or /where/) the partial elements were being
--     compared.

-- | Replaces any floating t'ConversionError's raised by the
-- continuation with the one generated (as per 'failConversion') from
-- the given arguments.
nowConversionChecking
  :: forall m a. (MonadTCError m, HasBuiltins m)
  => Comparison -- ^ Equality or subtyping?
  -> Term       -- ^ See 'convErrLhs'
  -> Term       -- ^ See 'convErrRhs'
  -> CompareAs  -- ^ Will be converted to a 'FailedCompareAs'.
  -> m a        -- ^ Generally, a recursive call to a type-specific conversion checking function.
  -> m a
nowConversionChecking :: forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a -> m a
nowConversionChecking Comparison
cmp Term
l Term
r CompareAs
cas m a
cont = m a
cont m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
  TypeError CallStack
loc TCState
st Closure{ clValue :: forall a. Closure a -> a
clValue = TypeError
err }
    | ConversionError_ ConversionError{ convErrCtx :: ConversionError -> ConversionErrorContext
convErrCtx = Floating{} } <- TypeError
err
    -> Comparison -> Term -> Term -> CompareAs -> m a
forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a
failConversion Comparison
cmp Term
l Term
r CompareAs
cas
  TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

-- | Freeze t'ConversionError's thrown by the continuation.
--
-- This function should be placed on the __inside__ of context updates.
cutConversionErrors
  :: (MonadPretty m, MonadError TCErr m)
  => m a -> m a
cutConversionErrors :: forall (m :: * -> *) a.
(MonadPretty m, MonadError TCErr m) =>
m a -> m a
cutConversionErrors m a
cont = m a
cont m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
  TypeError CallStack
loc TCState
st cl :: Closure TypeError
cl@Closure{ clValue :: forall a. Closure a -> a
clValue = ConversionError_ ConversionError
conv } -> Closure TypeError -> (TypeError -> m a) -> m a
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
cl \TypeError
_ ->
    ConversionError -> (ConversionError -> m a) -> m a
forall (m :: * -> *) z.
PureTCM m =>
ConversionError -> (ConversionError -> m z) -> m z
flattenConversionError ConversionError
conv \conv :: ConversionError
conv@ConversionError{convErrLhs :: ConversionError -> Term
convErrLhs = Term
lhs, convErrRhs :: ConversionError -> Term
convErrRhs = Term
rhs} -> do
      cl <- () -> m (Closure ())
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure ()
      throwError $ TypeError loc st $ cl $> case (lhs, rhs) of
        (Sort MetaS{} , Term
t            ) -> Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
        (Term
s            , Sort MetaS{} ) -> Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
        (Sort DefS{}  , Term
t            ) -> Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
        (Term
s            , Sort DefS{}  ) -> Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
        (Term, Term)
_                              -> ConversionError -> TypeError
ConversionError_ ConversionError
conv
  TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

-- | Intermediate type for storing the results of flattening a 'ConversionZipper'.
type ConversionProblem = (FailedCompareAs, Term, Term)

-- | @'eliminateLhsRhs' hd1 ty1 es1 hd2 ty2 es2@ generates a
-- @ConversionProblem@ between the mismatched terms @hd1@ and @hd2@,
-- which have the types @ty1@ and @ty2@ respectively.
--
-- If the types @ty1@ and @ty2@ respond to the given eliminations @es1@
-- and @es2@ respectively (which they should, since the inputs to
-- conversion checking are assumed to be well-typed), the mismatched
-- terms accumulate these, and the types are suitably refined.
--
-- Currently replaces large terms in the @es1@ by 'DontCare', as a HACK
-- to avoid the printing of big uncompared terms. In the future, this is
-- probably better handled in the reifier.
eliminateLhsRhs
  :: forall m. PureTCM m
  => Type -> Term -> Elims
  -> Type -> Term -> Elims
  -> m ConversionProblem
eliminateLhsRhs :: forall (m :: * -> *).
PureTCM m =>
Type
-> Term -> [Elim] -> Type -> Term -> [Elim] -> m ConversionProblem
eliminateLhsRhs Type
t1 Term
v1 [Elim]
l_es Type
t2 Term
v2 [Elim]
r_es =
  let
    blank :: Term -> Term
blank Term
t
      | Term -> Int
forall a. TermSize a => a -> Int
termSize Term
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
15 = Term -> Term
DontCare Term
t
      | Bool
otherwise        = Term
t
  in
  ConversionProblem
-> MaybeT m ConversionProblem -> m ConversionProblem
forall (m :: * -> *) a. Monad m => a -> MaybeT m a -> m a
fromMaybeT (Type -> Type -> FailedCompareAs
FailAsTermsOf Type
t1 Type
t2, Term
v1, Term
v2) do
    t1 <- MaybeT m Empty -> Term -> Type -> [Elim] -> MaybeT m Type
forall (m :: * -> *).
PureTCM m =>
m Empty -> Term -> Type -> [Elim] -> m Type
eliminateType MaybeT m Empty
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero Term
v1 Type
t1 [Elim]
l_es
    t2 <- eliminateType mzero v2 t2 r_es
    pure
      ( FailAsTermsOf t1 t2
      , v1 `applyE` map (fmap blank) l_es
      , v2 `applyE` map (fmap blank) r_es
      )

-- | @'mismatchedProjections' t1 v1 e1 t2 v2 e2@ raises a floating
-- conversion-checking error (as per 'failConversion') indicating that
-- the terms @v1@ and @v2@ (which have type @t1@ and @t2@ respectively,
-- and are typically neutral) disagree on the last elimination in their
-- spines.
--
-- The further eliminations @e1@ and @e2@ are treated as "uncompared"
-- context for the error message.
mismatchedProjections
  :: (MonadError TCErr m, PureTCM m)
  => Type  -- ^ LHS type, @t1@
  -> Term  -- ^ LHS term, @v1@; see 'convErrLhs'.
  -> Elims -- ^ Additional eliminations @e1@ present on the LHS beyond the failure of conversion checking
  -> Type  -- ^ RHS type, @t2@
  -> Term  -- ^ RHS term, @v2@; see 'convErrRhs'.
  -> Elims -- ^ Additional eliminations @e2@ present on the RHS beyond the failure of conversion checking
  -> m a
mismatchedProjections :: forall (m :: * -> *) a.
(MonadError TCErr m, PureTCM m) =>
Type -> Term -> [Elim] -> Type -> Term -> [Elim] -> m a
mismatchedProjections Type
t1 Term
v1 [Elim]
e1 Type
t2 Term
v2 [Elim]
e2 = do
  (tys, lhs, rhs) <- Type
-> Term -> [Elim] -> Type -> Term -> [Elim] -> m ConversionProblem
forall (m :: * -> *).
PureTCM m =>
Type
-> Term -> [Elim] -> Type -> Term -> [Elim] -> m ConversionProblem
eliminateLhsRhs Type
t1 Term
v1 [Elim]
e1 Type
t2 Term
v2 [Elim]
e2
  typeError $ ConversionError_ $ ConversionError CmpEq tys lhs rhs (Floating ConvStop)

-- | Compute a 'HeadMismatch' explaining why two terms disagree, if
-- there is a possibility that they might be printed identically.
headMismatch :: forall m. (PureTCM m, MonadPlus m) => Term -> Term -> m HeadMismatch
headMismatch :: forall (m :: * -> *).
(PureTCM m, MonadPlus m) =>
Term -> Term -> m HeadMismatch
headMismatch Var{}      Def{}      = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HeadMismatch
HdmVarDef
headMismatch Def{}      Var{}      = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HeadMismatch
HdmDefVar
headMismatch Var{}      Con{}      = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HeadMismatch
HdmVarCon
headMismatch Con{}      Var{}      = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HeadMismatch
HdmConVar
headMismatch (Var Int
i [Elim]
xs) (Var Int
j [Elim]
ys)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = Int -> Closure ([Elim], [Elim]) -> HeadMismatch
HdmVarSpine Int
i (Closure ([Elim], [Elim]) -> HeadMismatch)
-> m (Closure ([Elim], [Elim])) -> m HeadMismatch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Elim], [Elim]) -> m (Closure ([Elim], [Elim]))
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure ([Elim]
xs, [Elim]
ys)
headMismatch (Pi Dom Type
d1 Abs Type
_)  (Pi Dom Type
d2 Abs Type
_) =
  let
    hint :: (a -> a -> b) -> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
    hint :: forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint a -> a -> b
k forall x y. Dom' x y -> a
g a -> a -> Bool
c = a -> a -> b
k (Dom Type -> a
forall x y. Dom' x y -> a
g Dom Type
d1) (Dom Type -> a
forall x y. Dom' x y -> a
g Dom Type
d2) b -> m () -> m b
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (a -> a -> Bool
c (Dom Type -> a
forall x y. Dom' x y -> a
g Dom Type
d1) (Dom Type -> a
forall x y. Dom' x y -> a
g Dom Type
d2)))
  in WhyUnequalTypes -> HeadMismatch
HdmTypes (WhyUnequalTypes -> HeadMismatch)
-> m WhyUnequalTypes -> m HeadMismatch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m WhyUnequalTypes] -> m WhyUnequalTypes
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
    [ (Relevance -> Relevance -> WhyUnequalTypes)
-> (forall x y. Dom' x y -> Relevance)
-> (Relevance -> Relevance -> Bool)
-> m WhyUnequalTypes
forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint Relevance -> Relevance -> WhyUnequalTypes
forall a. (NFData a, Verbalize a) => a -> a -> WhyUnequalTypes
UnequalDomain     Dom' x y -> Relevance
forall a. LensRelevance a => a -> Relevance
forall x y. Dom' x y -> Relevance
getRelevance     Relevance -> Relevance -> Bool
sameRelevance
    , (Quantity -> Quantity -> WhyUnequalTypes)
-> (forall x y. Dom' x y -> Quantity)
-> (Quantity -> Quantity -> Bool)
-> m WhyUnequalTypes
forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint Quantity -> Quantity -> WhyUnequalTypes
forall a. (NFData a, Verbalize a) => a -> a -> WhyUnequalTypes
UnequalDomain     Dom' x y -> Quantity
forall a. LensQuantity a => a -> Quantity
forall x y. Dom' x y -> Quantity
getQuantity      Quantity -> Quantity -> Bool
sameQuantity
    , (PolarityModality -> PolarityModality -> WhyUnequalTypes)
-> (forall x y. Dom' x y -> PolarityModality)
-> (PolarityModality -> PolarityModality -> Bool)
-> m WhyUnequalTypes
forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint PolarityModality -> PolarityModality -> WhyUnequalTypes
forall a. (NFData a, Verbalize a) => a -> a -> WhyUnequalTypes
UnequalDomain     Dom' x y -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
forall x y. Dom' x y -> PolarityModality
getModalPolarity PolarityModality -> PolarityModality -> Bool
samePolarity
    , (Cohesion -> Cohesion -> WhyUnequalTypes)
-> (forall x y. Dom' x y -> Cohesion)
-> (Cohesion -> Cohesion -> Bool)
-> m WhyUnequalTypes
forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint Cohesion -> Cohesion -> WhyUnequalTypes
forall a. (NFData a, Verbalize a) => a -> a -> WhyUnequalTypes
UnequalDomain     Dom' x y -> Cohesion
forall a. LensCohesion a => a -> Cohesion
forall x y. Dom' x y -> Cohesion
getCohesion      Cohesion -> Cohesion -> Bool
sameCohesion
    , (Hiding -> Hiding -> WhyUnequalTypes)
-> (forall x y. Dom' x y -> Hiding)
-> (Hiding -> Hiding -> Bool)
-> m WhyUnequalTypes
forall a b.
(a -> a -> b)
-> (forall x y. Dom' x y -> a) -> (a -> a -> Bool) -> m b
hint Hiding -> Hiding -> WhyUnequalTypes
UnequalHiding     Dom' x y -> Hiding
forall a. LensHiding a => a -> Hiding
forall x y. Dom' x y -> Hiding
getHiding        Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding
    ]
headMismatch (Def QName
i [Elim]
_)  (Def QName
j [Elim]
_)
  | QName -> Bool
isExtendedLambdaName QName
i, QName -> Bool
isExtendedLambdaName QName
j = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HeadMismatch -> m HeadMismatch) -> HeadMismatch -> m HeadMismatch
forall a b. (a -> b) -> a -> b
$ QName -> QName -> HeadMismatch
HdmExtLam QName
i QName
j
headMismatch (Var Int
i [Elim]
xs) (Var Int
j [Elim]
ys) = HeadMismatch -> m HeadMismatch
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HeadMismatch -> m HeadMismatch) -> HeadMismatch -> m HeadMismatch
forall a b. (a -> b) -> a -> b
$ Int -> Int -> HeadMismatch
HdmVars Int
i Int
j
headMismatch Term
lhs        Term
rhs        = do
  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.ctx" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"headMismatch no match"
    , TCMT IO Doc
"  lhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs
    , TCMT IO Doc
"  rhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs
    ]
  m HeadMismatch
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | Flatten a Floating conversion checking error into one that
-- presents interesting context around the failing terms.
--
-- The continuation is only invoked with 'Finished' t'ConversionError's.
flattenConversionError :: forall m z. PureTCM m => ConversionError -> (ConversionError -> m z) -> m z
flattenConversionError :: forall (m :: * -> *) z.
PureTCM m =>
ConversionError -> (ConversionError -> m z) -> m z
flattenConversionError e :: ConversionError
e@ConversionError{convErrCtx :: ConversionError -> ConversionErrorContext
convErrCtx = Finished{}} ConversionError -> m z
cont = ConversionError -> m z
cont ConversionError
e
flattenConversionError (ConversionError Comparison
cmp FailedCompareAs
tys Term
lhs Term
rhs (Floating ConversionZipper
ctx)) ConversionError -> m z
cont =
  do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.ctx" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"unwinding conversion zipper:"
      , TCMT IO Doc
"  env:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope)
      , TCMT IO Doc
"  tys:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> FailedCompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => FailedCompareAs -> m Doc
prettyTCM FailedCompareAs
tys
      , TCMT IO Doc
"  lhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs
      , TCMT IO Doc
"  rhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs
      , TCMT IO Doc
"  zip:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConversionZipper -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM ConversionZipper
ctx
      ]
    let
      k :: HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
k HereOrThere
ht Maybe HeadMismatch
hdm (FailedCompareAs
tys, Term
lhs, Term
rhs) = do
        String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.ctx" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"conversion zipper unwound:"
          , TCMT IO Doc
"  env:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope)
          , TCMT IO Doc
"  tys:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> FailedCompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => FailedCompareAs -> m Doc
prettyTCM FailedCompareAs
tys
          , TCMT IO Doc
"  lhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lhs
          , TCMT IO Doc
"  rhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs
          , TCMT IO Doc
"  hdm:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Maybe HeadMismatch -> String
forall a. Show a => a -> String
show Maybe HeadMismatch
hdm)
          ]
        ConversionError -> m z
cont (Comparison
-> FailedCompareAs
-> Term
-> Term
-> ConversionErrorContext
-> ConversionError
ConversionError Comparison
cmp FailedCompareAs
tys Term
lhs Term
rhs (HereOrThere -> Maybe HeadMismatch -> ConversionErrorContext
Finished HereOrThere
ht Maybe HeadMismatch
hdm))
    (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
k ConversionZipper
ctx
  where

  -- Actually apply the continuation. This is the innermost function in
  -- handling the ConversionProblem, so this is our opportunity to
  -- collect any headMismatch information that might get buried in
  -- backtrace terms.
  done :: forall z. (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z) -> m z
  done :: forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
done HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok = do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.ctx" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"reached center of conversion zipper:"
      , TCMT IO Doc
"  env:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope)
      , TCMT IO Doc
"  tys:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> FailedCompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => FailedCompareAs -> m Doc
prettyTCM FailedCompareAs
tys
      , TCMT IO Doc
"  lhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
lhs
      , TCMT IO Doc
"  rhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
rhs
      ]
    hdm <- MaybeT m HeadMismatch -> m (Maybe HeadMismatch)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m HeadMismatch -> m (Maybe HeadMismatch))
-> MaybeT m HeadMismatch -> m (Maybe HeadMismatch)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> MaybeT m HeadMismatch
forall (m :: * -> *).
(PureTCM m, MonadPlus m) =>
Term -> Term -> m HeadMismatch
headMismatch Term
lhs Term
rhs
    ok Here hdm (tys, lhs, rhs)

  -- Discard an uninteresting prefix of call stack (anything that does
  -- not mention an implicit argument), moving any binders from the
  -- zipper to the context of the continuation.
  seek
    :: forall z.  (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
    -> ConversionZipper
    -> m z
  seek :: forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok ConversionZipper
zip = case ConversionZipper
zip of
    ConversionZipper
ConvStop -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
done HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok
    ConvApply Term
hd Abs Type
ty (Arg ArgInfo
info ConversionZipper
rest) [Elim]
l_es [Elim]
r_es
      | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info                                   -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok ConversionZipper
rest
      | Con ConHead
c ConInfo
o [Elim]
_ <- Term
hd, IsRecord{} <- ConHead -> DataOrRecord' PatternOrCopattern
conDataRecord ConHead
c -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok ConversionZipper
rest
    ConvLam Dom Type
dom Abs ()
ty String
name ConversionZipper
rest -> (String, Dom Type) -> m z -> m z
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) (m z -> m z) -> m z -> m z
forall a b. (a -> b) -> a -> b
$ (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok ConversionZipper
rest
    ConvCod Dom Type
dom String
name ConversionZipper
rest    -> (String, Dom Type) -> m z -> m z
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) (m z -> m z) -> m z -> m z
forall a b. (a -> b) -> a -> b
$ (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok ConversionZipper
rest
    ConvDom Dom ConversionZipper
dom Abs Type
c1 Abs Type
c2        -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> ConversionZipper -> m z
seek HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok (Dom ConversionZipper -> ConversionZipper
forall t e. Dom' t e -> e
unDom Dom ConversionZipper
dom)
    ConversionZipper
_ -> ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify ConversionZipper
zip (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok HereOrThere
Here) HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok

  -- Actually reifies a 'ConversionZipper' as a term around the conversion
  -- problem.
  -- This function takes both a success continuation (with three
  -- arguments) and a failing continuation, in case we had to give up on
  -- building the context term.
  reify
    :: forall z. ConversionZipper
    -> (Maybe HeadMismatch -> ConversionProblem -> m z)
    -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
    -> m z
  reify :: forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify ConversionZipper
ctx Maybe HeadMismatch -> ConversionProblem -> m z
err HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok = case ConversionZipper
ctx of
    -- Empty call stack, nothing to do
    ConversionZipper
ConvStop -> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
(HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
done HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok

    -- Going under binders.
    --
    -- These both function in the same way, though the lambda case seems
    -- much bigger because it has to update the expected types.
    --
    -- On the failure continuation, since we're not building a term
    -- wrapper to add any variables that are referred to by the
    -- mismatched terms, we have to move the binders into the context.
    --
    -- On the success continuation, the term binder is added, and (if
    -- possible) the comparison is updated for accuracy.
    ConvCod Dom Type
dom String
name ConversionZipper
rest -> ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify ConversionZipper
rest (\Maybe HeadMismatch
hdm ConversionProblem
prob -> (String, Dom Type) -> m z -> m z
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) (m z -> m z) -> m z -> m z
forall a b. (a -> b) -> a -> b
$ Maybe HeadMismatch -> ConversionProblem -> m z
err Maybe HeadMismatch
hdm ConversionProblem
prob)
      \HereOrThere
_ Maybe HeadMismatch
hdm (FailedCompareAs
_, Term
lhs, Term
rhs) -> HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok HereOrThere
There Maybe HeadMismatch
hdm
        ( FailedCompareAs
FailAsTypes
        , Dom Type -> Abs Type -> Term
Pi Dom Type
dom (String -> Type -> Abs Type
forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs String
name (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ Term
lhs))
        , Dom Type -> Abs Type -> Term
Pi Dom Type
dom (String -> Type -> Abs Type
forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs String
name (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ Term
rhs))
        )

    ConvLam Dom Type
dom Abs ()
ty String
name ConversionZipper
rest -> ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify ConversionZipper
rest
      (\Maybe HeadMismatch
hdm ConversionProblem
prob -> (String, Dom Type) -> m z -> m z
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) (m z -> m z) -> m z -> m z
forall a b. (a -> b) -> a -> b
$ Maybe HeadMismatch -> ConversionProblem -> m z
err Maybe HeadMismatch
hdm ConversionProblem
prob)
      \HereOrThere
ht Maybe HeadMismatch
hdm (FailedCompareAs
cmp, Term
lhs, Term
rhs) -> HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok HereOrThere
There Maybe HeadMismatch
hdm
        ( case FailedCompareAs
cmp of
            -- Ideally it would be provably impossible for a 'ConvLam'
            -- to be on the stack after an untyped comparison, but I
            -- can't be sure that this is actually the case.
            --
            -- If it does happen, it's safer to print a stupid-looking
            -- error (the types λ x → ... and λ x → ... are not equal)
            -- than it is to print an error with dummy terms.
            --
            -- And if someone complains about the error being stupid, we
            -- hopefully get a test case to fix it with.
            FailedCompareAs
FailAsTypes       -> FailedCompareAs
FailAsTypes
            -- If we do have the expected types then we can just wrap
            -- them in Pi types.
            FailAsTermsOf Type
a Type
b -> Type -> Type -> FailedCompareAs
FailAsTermsOf
              (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) (Dom Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Dom Type
dom) (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a Sort' Term -> Abs () -> Abs (Sort' Term)
forall a b. a -> Abs b -> Abs a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs ()
ty)) (Dom Type -> Abs Type -> Term
Pi Dom Type
dom (Type
a Type -> Abs () -> Abs Type
forall a b. a -> Abs b -> Abs a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs ()
ty)))
              (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) (Dom Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Dom Type
dom) (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
b Sort' Term -> Abs () -> Abs (Sort' Term)
forall a b. a -> Abs b -> Abs a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs ()
ty)) (Dom Type -> Abs Type -> Term
Pi Dom Type
dom (Type
b Type -> Abs () -> Abs Type
forall a b. a -> Abs b -> Abs a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs ()
ty)))
        , ArgInfo -> Abs Term -> Term
Lam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (String -> Term -> Abs Term
forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs String
name Term
lhs), ArgInfo -> Abs Term -> Term
Lam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (String -> Term -> Abs Term
forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs String
name Term
rhs)
        )

    -- Entering the domain of a function type. Bolts the codomains onto
    -- the failing term. No context handling is needed.
    ConvDom Dom ConversionZipper
dom Abs Type
c1 Abs Type
c2 -> ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify (Dom ConversionZipper -> ConversionZipper
forall t e. Dom' t e -> e
unDom Dom ConversionZipper
dom) Maybe HeadMismatch -> ConversionProblem -> m z
err \HereOrThere
_ Maybe HeadMismatch
hdm (FailedCompareAs
_, Term
lhs, Term
rhs) -> HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok HereOrThere
There Maybe HeadMismatch
hdm
      ( FailedCompareAs
FailAsTypes
      , Dom Type -> Abs Type -> Term
Pi (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ Term
lhs Type -> Dom ConversionZipper -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ConversionZipper
dom) Abs Type
c1
      , Dom Type -> Abs Type -> Term
Pi (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ Term
rhs Type -> Dom ConversionZipper -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ConversionZipper
dom) Abs Type
c2
      )

    -- Entering an argument to a neutral.
    ConvApply Term
hd Abs Type
ty (Arg ArgInfo
info ConversionZipper
rest) [Elim]
l_es [Elim]
r_es -> ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
forall z.
ConversionZipper
-> (Maybe HeadMismatch -> ConversionProblem -> m z)
-> (HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z)
-> m z
reify ConversionZipper
rest Maybe HeadMismatch -> ConversionProblem -> m z
err \HereOrThere
_ Maybe HeadMismatch
hdm prob :: ConversionProblem
prob@(FailedCompareAs
_, Term
lhs', Term
rhs') ->
      let info' :: ArgInfo
info' = ArgInfo
info { argInfoOrigin = ConversionFail } in case Term
hd of

        -- If the argument is to an extended lambda, we give up on
        -- reifying this frame (and anything it would return to) since
        -- that generally makes the error messages *worse*.
        -- This is the purpose of passing the failing continuation
        -- around.
        Def QName
nm [Elim]
as | QName -> Bool
isExtendedLambdaName QName
nm -> do
          ~Function{ funExtLam = Just (ExtLamInfo m b sys) } <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
nm
          bs <- lookupSection m
          reportSDoc "tc.conv.ctx" 30 $ vcat
            [ "conversion context has extended lambda" <+> pretty nm
            , "bs " <> parens (pretty (size bs)) <> colon <> " " <> pretty bs
            , "as " <> parens (pretty (size as)) <> colon <> " " <> pretty as
            ]
          err hdm prob

        -- Otherwise, we just build the function call. Note that the
        -- ArgInfo is updated so that the reifier will print the
        -- mismatched term in case it happens in an implicit argument.
        Term
_ -> HereOrThere -> Maybe HeadMismatch -> ConversionProblem -> m z
ok HereOrThere
There Maybe HeadMismatch
hdm (ConversionProblem -> m z) -> m ConversionProblem -> m z
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type
-> Term -> [Elim] -> Type -> Term -> [Elim] -> m ConversionProblem
forall (m :: * -> *).
PureTCM m =>
Type
-> Term -> [Elim] -> Type -> Term -> [Elim] -> m ConversionProblem
eliminateLhsRhs
          (Abs Type
ty Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
lhs') (Term
hd Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Term
lhs']) [Elim]
l_es
          (Abs Type
ty Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
rhs') (Term
hd Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Term
rhs']) [Elim]
r_es

instance PrettyTCM FailedCompareAs where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => FailedCompareAs -> m Doc
prettyTCM = \case
    FailAsTypes{}     -> m Doc
"(as types)"
    FailAsTermsOf Type
a Type
b -> 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma 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
b

instance PrettyTCM ConversionZipper where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM = \case
    ConversionZipper
ConvStop -> m Doc
"<>"
    ConvLam Dom Type
dom Abs ()
ret String
nm ConversionZipper
rest -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"lam"   m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty String
nm m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
dom
      , m Doc
"ret: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs () -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs ()
ret
      , m Doc
"rest:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (ConversionZipper -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM ConversionZipper
rest)
      ]
    ConvCod Dom Type
dom String
nm ConversionZipper
rest -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"cod"   m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty String
nm m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
dom
      , m Doc
"rest:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (ConversionZipper -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM ConversionZipper
rest)
      ]
    ConvDom Dom ConversionZipper
dom Abs Type
t1 Abs Type
t2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"dom:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom' Term () -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (() () -> Dom ConversionZipper -> Dom' Term ()
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom ConversionZipper
dom)
      , m Doc
"t1: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Type
t1
      , m Doc
"t2: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Type
t2
      , m Doc
"rest:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (ConversionZipper -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM (Dom ConversionZipper -> ConversionZipper
forall t e. Dom' t e -> e
unDom Dom ConversionZipper
dom))
      ]
    ConvApply Term
hd Abs Type
ty (Arg ArgInfo
info ConversionZipper
rest) [Elim]
lhs [Elim]
rhs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"apply" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
hd
      , m Doc
"ty:  " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Type
ty
      , m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim] -> m Doc
prettyTCM [Elim]
lhs
      , m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim] -> m Doc
prettyTCM [Elim]
rhs
      , m Doc
"rest:"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (ConversionZipper -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConversionZipper -> m Doc
prettyTCM ConversionZipper
rest)
      ]

instance PrettyTCM ConversionError where
  prettyTCM :: forall m. MonadPretty m => ConversionError -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ConversionError -> m Doc
prettyTCM ConversionError
err = ConversionError -> (ConversionError -> m Doc) -> m Doc
forall (m :: * -> *) z.
PureTCM m =>
ConversionError -> (ConversionError -> m z) -> m z
flattenConversionError ConversionError
err \(ConversionError Comparison
cmp FailedCompareAs
tys Term
lhs Term
rhs ~(Finished HereOrThere
ht Maybe HeadMismatch
hdm)) -> do
    (d1, d2, disamb) <- HereOrThere
-> Maybe HeadMismatch -> Term -> Term -> m (Doc, Doc, Maybe Doc)
forall (m :: * -> *).
MonadPretty m =>
HereOrThere
-> Maybe HeadMismatch -> Term -> Term -> m (Doc, Doc, Maybe Doc)
prettyInEqual HereOrThere
ht Maybe HeadMismatch
hdm Term
lhs Term
rhs
    let
      disambs = 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
$ Maybe (m Doc) -> m Doc
forall a. Null a => Maybe a -> a
orEmpty (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Maybe Doc -> Maybe (m Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Doc
disamb)
      what = Maybe HeadMismatch
hdm Maybe HeadMismatch
-> (HeadMismatch -> Maybe WhyUnequalTypes) -> Maybe WhyUnequalTypes
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        HdmTypes WhyUnequalTypes
x -> WhyUnequalTypes -> Maybe WhyUnequalTypes
forall a. a -> Maybe a
Just WhyUnequalTypes
x
        HeadMismatch
_          -> Maybe WhyUnequalTypes
forall a. Maybe a
Nothing
    case tys of
      FailAsTermsOf Type
lhs_t Type
rhs_t -> BlockT m Bool -> m (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Type -> Type -> BlockT m Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Type -> m Bool
pureEqualType Type
lhs_t Type
rhs_t) m (Either Blocker Bool) -> (Either Blocker Bool -> m Doc) -> m Doc
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Bool
True -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ m Doc
"The terms", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1)
          , m Doc
"and",       Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2)
          , m Doc
"are not equal at 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
lhs_t m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Maybe (m Doc) -> m Doc
forall a. Null a => Maybe a -> a
orEmpty (m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"because:" m Doc -> Maybe Doc -> Maybe (m Doc)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Doc
disamb)
          , m Doc
disambs
          ]
        Either Blocker Bool
_ -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ m Doc
"The terms", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1 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
lhs_t)
          , m Doc
"and",       Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2 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
rhs_t)
          , m Doc
"are not equal" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Maybe (m Doc) -> m Doc
forall a. Null a => Maybe a -> a
orEmpty (m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"because:" m Doc -> Maybe Doc -> Maybe (m Doc)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Doc
disamb)
          , m Doc
disambs
          ]
      FailedCompareAs
FailAsTypes | Comparison
CmpEq <- Comparison
cmp -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"The" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Maybe WhyUnequalTypes
what of
            Just UnequalDomain{} -> m Doc
"function types"
            Just UnequalHiding{} -> m Doc
"function types"
            Maybe WhyUnequalTypes
_ -> m Doc
"types"
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1), m Doc
"and", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2)
        , m Doc
"are not equal" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Maybe (m Doc) -> m Doc
forall a. Null a => Maybe a -> a
orEmpty (m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"because:" m Doc -> Maybe Doc -> Maybe (m Doc)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Doc
disamb)
        , m Doc
disambs
        ]
      FailedCompareAs
FailAsTypes | Comparison
CmpLeq <- Comparison
cmp -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"The" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Maybe WhyUnequalTypes
what of
            Just UnequalDomain{} -> m Doc
"function type"
            Just UnequalHiding{} -> m Doc
"function type"
            Maybe WhyUnequalTypes
_ -> m Doc
"type"
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1), m Doc
"is not a subtype of", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2)
        , Maybe (m Doc) -> m Doc
forall a. Null a => Maybe a -> a
orEmpty (m Doc
"because:" m Doc -> Maybe Doc -> Maybe (m Doc)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Doc
disamb)
        , m Doc
disambs
        ]

-- | Pretty print a pair of distinct terms @t1@ and @t2@, producing a
-- disambiguator if the terms render the same with the ambient settings
-- but differently with display forms.
displayDisamb
  :: forall m. MonadPretty m
  => HereOrThere                         -- ^ For grammar
  -> Maybe (Int, Closure (Elims, Elims))
    -- ^ From a 'HeadMismatch', to indicate what projections' display
    -- forms caused the rerender (if any)
  -> Term -- ^ @t1@
  -> Term -- ^ @t2@
  -> m (Doc, Doc, Maybe Doc)
displayDisamb :: forall (m :: * -> *).
MonadPretty m =>
HereOrThere
-> Maybe (Int, Closure ([Elim], [Elim]))
-> Term
-> Term
-> m (Doc, Doc, Maybe Doc)
displayDisamb HereOrThere
ht Maybe (Int, Closure ([Elim], [Elim]))
hdm Term
t1 Term
t2 = do
  d1 <- Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t1
  d2 <- prettyTCMCtx TopCtx t2
  let
    maybeProjs :: Elims -> Elims -> MaybeT m [m Doc]
    maybeProjs (Proj ProjOrigin
_ QName
p:[Elim]
xs) (Proj ProjOrigin
_ QName
p':[Elim]
ys) | QName
p QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
p' = do
      df  <- QName -> MaybeT m Bool
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Bool
hasDisplayForms QName
p
      df' <- hasDisplayForms p'
      case (df, df') of
        (Bool
True, Bool
False)  -> [m Doc] -> MaybeT m [m Doc]
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([m Doc] -> MaybeT m [m Doc]) -> [m Doc] -> MaybeT m [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a display form for" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup 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
p, m Doc
"has"]
        (Bool
False, Bool
True)  -> [m Doc] -> MaybeT m [m Doc]
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([m Doc] -> MaybeT m [m Doc]) -> [m Doc] -> MaybeT m [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"a display form for" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup 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
p', m Doc
"has"]
        (Bool
True, Bool
True)   -> [m Doc] -> MaybeT m [m Doc]
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([m Doc] -> MaybeT m [m Doc]) -> [m Doc] -> MaybeT m [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"display forms for"  [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup 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
p, m Doc
"and", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p', m Doc
"have"]
        (Bool
False, Bool
False) -> MaybeT m [m Doc]
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    maybeProjs (Elim
_:[Elim]
xs) (Elim
_:[Elim]
ys) = [Elim] -> [Elim] -> MaybeT m [m Doc]
maybeProjs [Elim]
xs [Elim]
ys
    maybeProjs [Elim]
_ [Elim]
_           = MaybeT m [m Doc]
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

  (d1, d2,) <$> runMaybeT do
    guard (P.render d1 == P.render d2)
    reportSDoc "tc.error.conv" 30 $ vcat
      [ "terms rendered the same"
      , "  t1:" <+> pretty t1
      , "  d1:" <+> pure d1
      , "  t2:" <+> pretty t2
      , "  d2:" <+> pure d2
      ]

    (d1, d2) <- locallyTC eDisplayFormsEnabled (const False) do
      (,) <$> prettyTCMCtx TopCtx t1 <*> prettyTCMCtx TopCtx t2
    guard (P.render d1 /= P.render d2)

    whatdf <- case hdm of
      Just (Int
_, Closure ([Elim], [Elim])
cl) -> Closure ([Elim], [Elim])
-> (([Elim], [Elim]) -> MaybeT m (Maybe [m Doc]))
-> MaybeT m (Maybe [m Doc])
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure ([Elim], [Elim])
cl (m (Maybe [m Doc]) -> MaybeT m (Maybe [m Doc])
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe [m Doc]) -> MaybeT m (Maybe [m Doc]))
-> (([Elim], [Elim]) -> m (Maybe [m Doc]))
-> ([Elim], [Elim])
-> MaybeT m (Maybe [m Doc])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m [m Doc] -> m (Maybe [m Doc])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m [m Doc] -> m (Maybe [m Doc]))
-> (([Elim], [Elim]) -> MaybeT m [m Doc])
-> ([Elim], [Elim])
-> m (Maybe [m Doc])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Elim] -> [Elim] -> MaybeT m [m Doc])
-> ([Elim], [Elim]) -> MaybeT m [m Doc]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Elim] -> [Elim] -> MaybeT m [m Doc]
maybeProjs) MaybeT m (Maybe [m Doc])
-> (Maybe [m Doc] -> [m Doc]) -> MaybeT m [m Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
        [m Doc] -> Maybe [m Doc] -> [m Doc]
forall a. a -> Maybe a -> a
fromMaybe (String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"display forms have")
      Maybe (Int, Closure ([Elim], [Elim]))
Nothing      -> [m Doc] -> MaybeT m [m Doc]
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([m Doc] -> MaybeT m [m Doc]) -> [m Doc] -> MaybeT m [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"display forms have"

    vcat
      [ fsep $ map lift whatdf <> pwords "caused" <> pwords case ht of
          HereOrThere
Here  -> String
"them"
          HereOrThere
There -> String
"the mismatched terms"
      , nest 2 (pure d1), "and", nest 2 (pure d2)
      , "to render the same"
      ]


-- | Print two terms that are supposedly unequal, additionally returning
-- an explanation (informed by the HeadMismatch) if they happened to
-- print to the same thing.
prettyInEqual
  :: MonadPretty m
  => HereOrThere        -- ^ For grammar
  -> Maybe HeadMismatch -- ^ Collected disambiguator information
  -> Term -> Term -> m (Doc, Doc, Maybe Doc)
prettyInEqual :: forall (m :: * -> *).
MonadPretty m =>
HereOrThere
-> Maybe HeadMismatch -> Term -> Term -> m (Doc, Doc, Maybe Doc)
prettyInEqual HereOrThere
ht Maybe HeadMismatch
hdm Term
t1 Term
t2
  -- If we don't know why they differ, or the mismatched terms are
  -- headed by the same variable, we defer to 'displayDisamb' which is
  -- capable of rendering the term without display forms to fish for an
  -- improvement in printing.
  | Maybe HeadMismatch
Nothing                 <- Maybe HeadMismatch
hdm = HereOrThere
-> Maybe (Int, Closure ([Elim], [Elim]))
-> Term
-> Term
-> m (Doc, Doc, Maybe Doc)
forall (m :: * -> *).
MonadPretty m =>
HereOrThere
-> Maybe (Int, Closure ([Elim], [Elim]))
-> Term
-> Term
-> m (Doc, Doc, Maybe Doc)
displayDisamb HereOrThere
ht Maybe (Int, Closure ([Elim], [Elim]))
forall a. Maybe a
Nothing Term
t1 Term
t2
  | Just (HdmVarSpine Int
i Closure ([Elim], [Elim])
cl) <- Maybe HeadMismatch
hdm = HereOrThere
-> Maybe (Int, Closure ([Elim], [Elim]))
-> Term
-> Term
-> m (Doc, Doc, Maybe Doc)
forall (m :: * -> *).
MonadPretty m =>
HereOrThere
-> Maybe (Int, Closure ([Elim], [Elim]))
-> Term
-> Term
-> m (Doc, Doc, Maybe Doc)
displayDisamb HereOrThere
ht ((Int, Closure ([Elim], [Elim]))
-> Maybe (Int, Closure ([Elim], [Elim]))
forall a. a -> Maybe a
Just (Int
i, Closure ([Elim], [Elim])
cl)) Term
t1 Term
t2

  -- If they're distinct function types, we don't have to bother
  -- rerendering.
  | Just (HdmTypes WhyUnequalTypes
x)       <- Maybe HeadMismatch
hdm =
    let
      ecore :: [m Doc]
ecore = case WhyUnequalTypes
x of
        UnequalDomain a
a a
b -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one has"
          [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 (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Verbalize a => a -> String
verbalize a
a))]
          [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
"domain, while the other is"
          [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 (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Verbalize a => a -> String
verbalize a
b)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
        UnequalHiding Hiding
a Hiding
b -> String -> [m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one takes"
          [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 (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Indefinite Hiding -> String
forall a. Verbalize a => a -> String
verbalize (Hiding -> Indefinite Hiding
forall a. a -> Indefinite a
Indefinite Hiding
a)))]
          [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
"argument, while the other takes"
          [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 (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Indefinite Hiding -> String
forall a. Verbalize a => a -> String
verbalize (Hiding -> Indefinite Hiding
forall a. a -> Indefinite a
Indefinite Hiding
b))), m Doc
"argument."]
      explain :: m Doc
explain = case HereOrThere
ht of
        HereOrThere
Here  -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [m Doc]
ecore
        HereOrThere
There -> [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
"the mismatched terms are function types;" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc]
ecore
    in (,,) (Doc -> Doc -> Maybe Doc -> (Doc, Doc, Maybe Doc))
-> m Doc -> m (Doc -> Maybe Doc -> (Doc, Doc, Maybe Doc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t1 m (Doc -> Maybe Doc -> (Doc, Doc, Maybe Doc))
-> m Doc -> m (Maybe Doc -> (Doc, Doc, Maybe Doc))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t2 m (Maybe Doc -> (Doc, Doc, Maybe Doc))
-> m (Maybe Doc) -> m (Doc, Doc, Maybe Doc)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> m Doc -> m (Maybe Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
explain)

-- If it's some other class of mismatch, a rerender would probably not
-- improve things.
prettyInEqual HereOrThere
ht (Just HeadMismatch
hdm) Term
t1 Term
t2 = do
  d1 <- Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t1
  d2 <- prettyTCMCtx TopCtx t2
  (d1, d2,) <$> runMaybeT do
    guard (P.render d1 == P.render d2)
    let
      mm = case HereOrThere
ht of
        HereOrThere
Here  -> []
        HereOrThere
There -> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"of the mismatched terms"
    case hdm of
      HdmExtLam QName
a QName
b -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$
          case HereOrThere
ht of
            HereOrThere
Here  -> MaybeT m Doc -> [MaybeT m Doc]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeT m Doc
"they"
            HereOrThere
There -> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"the mismatched terms"
          [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"are distinct extended lambdas; "
        , String -> MaybeT m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"one is defined at"
        , MaybeT m Doc
"  " MaybeT m Doc -> MaybeT m Doc -> MaybeT m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> MaybeT m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Name -> Range
nameBindingSite (QName -> Name
qnameName QName
a))
        , String -> MaybeT m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"and the other at"
        , MaybeT m Doc
"  " MaybeT m Doc -> MaybeT m Doc -> MaybeT m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Range -> MaybeT m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Name -> Range
nameBindingSite (QName -> Name
qnameName QName
b)) MaybeT m Doc -> MaybeT m Doc -> MaybeT m Doc
forall a. Semigroup a => a -> a -> a
<> MaybeT m Doc
",")
        , String -> MaybeT m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"so they have different internal representations."
        ]

      HeadMismatch
HdmVarDef   -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$ String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [MaybeT m Doc]
mm [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is a variable, the other a definition"
      HeadMismatch
HdmVarCon   -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$ String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [MaybeT m Doc]
mm [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is a variable, the other a constructor"
      HeadMismatch
HdmDefVar   -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$ String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [MaybeT m Doc]
mm [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is a definition, the other a variable"
      HeadMismatch
HdmConVar   -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$ String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [MaybeT m Doc]
mm [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is a constructor, the other a variable"
      HdmVars Int
i Int
j -> [MaybeT m Doc] -> MaybeT m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([MaybeT m Doc] -> MaybeT m Doc) -> [MaybeT m Doc] -> MaybeT m Doc
forall a b. (a -> b) -> a -> b
$
           String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"one" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [MaybeT m Doc]
mm [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"has de Bruijn index "
        [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [Int -> MaybeT m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
i MaybeT m Doc -> MaybeT m Doc -> MaybeT m Doc
forall a. Semigroup a => a -> a -> a
<> MaybeT m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> String -> [MaybeT m Doc]
forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"the other" [MaybeT m Doc] -> [MaybeT m Doc] -> [MaybeT m Doc]
forall a. Semigroup a => a -> a -> a
<> [Int -> MaybeT m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
j]