Monad.hs

{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards   #-}

-- | The checker's monad.
--
-- @TypeCheck n@ is the old @TypeCheck var@ with the scope index in place of the
-- variable type. The error channel, though, is /not/ indexed: an error carries
-- the context it was raised in (see "Rzk.TypeCheck.Error"). That is what makes
-- 'inContext' a one-liner — running a judgement in an inner scope is just running
-- it under a different reader, with nothing to re-index on the way out. The old
-- @closeScope@ had to wrap the error one binder deeper and re-emit the holes.
module Rzk.TypeCheck.Monad where

import           Control.Monad            (unless, when)
import           Control.Monad.Except     (ExceptT,
                                           MonadError (catchError, throwError),
                                           runExceptT)
import           Control.Monad.Reader     (ReaderT (..), ask, asks, local)
import           Control.Monad.Trans      (lift)
import           Control.Monad.Trans.State.Strict (State, get, modify', put,
                                           runState)
import qualified Data.IntMap.Strict       as IntMap
import qualified Data.IntSet              as IntSet
import           Debug.Trace              (trace)

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil

import           Language.Rzk.Foil.Names (TModality, VarIdent)
import           Language.Rzk.Foil.Syntax (positionOfTerm)
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display
import           Rzk.TypeCheck.Error

-- | A binding shown in a hole's local context: the display name and its type,
-- already rendered.
data HoleEntry = HoleEntry
  { holeEntryName :: VarIdent
  , holeEntryType :: Rendered
  , holeEntryMode :: HoleModalInfo
  } deriving (Eq, Show)

data HoleModalInfo = HoleModalInfo
  { holeItemModality   :: TModality
  , holeItemLocks      :: TModality
  , holeItemAccessible :: Bool
  } deriving (Eq, Show)

data HoleTopeEntry = HoleTopeEntry
  { holeTopeValue :: Rendered
  , holeTopeMode  :: HoleModalInfo
  } deriving (Eq, Show)

-- | The structured goal and context at a hole, recorded in lenient mode (see
-- 'allowHoles'). Everything is rendered to user-facing names at record time, so
-- 'HoleInfo' is independent of the scope it came from. Local hypotheses are split
-- into ordinary term variables and cube variables (the cube/tope layer is
-- specific to Rzk); the global environment is deliberately excluded — it belongs
-- in a searchable inventory, not the goal panel.
data HoleInfo = HoleInfo
  { holeName          :: Maybe VarIdent -- ^ the @?name@, if the hole was named
  , holeGoal          :: Rendered       -- ^ expected type (the goal), kept symbolic
  , holeGoalShape     :: Maybe (VarIdent, Rendered)
    -- ^ when the goal is a /shape/ (the hole is the argument of a
    -- shape-restricted function), the shape's bound variable and its tope: the
    -- goal then reads @(binder : holeGoal | tope)@. 'Nothing' for an ordinary
    -- goal. (Extension-type goals need no special handling — they are already a
    -- restricted type in 'holeGoal'.)
  , holeTermVars      :: [HoleEntry]    -- ^ local hypotheses whose type is not a cube
  , holeCubeVars      :: [HoleEntry]    -- ^ local cube variables (type is a cube)
  , holeTopes         :: [HoleTopeEntry] -- ^ local tope assumptions (excluding ⊤)
  , holeCandidates    :: [Rendered]
    -- ^ Rendered moves from local hypotheses, allow-listed top-level lemmas,
    -- and tope-context elimination; missing subterms remain holes.
  , holeIntroductions :: [Rendered]
    -- ^ introduction forms for the goal type, built from its head constructor
    -- with the constituents left as holes. Already rendered, like the rest.
  , holeDiagram       :: Maybe String
    -- ^ an SVG of the goal cell, when the goal is a renderable shape (an arrow,
    -- triangle, or square up to dimension 3).
  , holeLocation      :: Maybe LocationInfo
  } deriving (Eq, Show)

-- | A structured checker diagnostic. Safe error mode rejects fragment violations.
data CheckWarning
  = LargeInductiveTypeWarning
      VarIdent              -- ^ the data type
      VarIdent              -- ^ the constructor whose field stores a universe
      (Maybe LocationInfo)
  | MetaPrefixWarning
      VarIdent              -- ^ the declaration whose type or body contains the use
      VarIdent              -- ^ the declaration used with too few meta-prefix arguments
      Int                   -- ^ the arguments supplied
      Int                   -- ^ the length of the meta prefix
      MetaPrefixRule
      (Maybe LocationInfo)
  | RSTTScopeWarning RSTTExtension String (Maybe LocationInfo)
  | RSTTHoleWarning (Maybe LocationInfo)
  | RSTTIncompleteWarning String (Maybe LocationInfo)
  | OverhangWarning
      String                -- ^ restriction face or recOR branch guard
      String                -- ^ the face or guard, rendered
      [String]              -- ^ the local tope context, rendered
      (Maybe LocationInfo)
  | TopeFamilyDomainWarning
      String                -- ^ the family, rendered where it was checked
      String                -- ^ its declared domain, rendered under the family's binder
      (Maybe LocationInfo)
  | FreeStandingRestrictionWarning
      VarIdent              -- ^ the declaration
      String                -- ^ the restricted type, rendered
      FragmentUse           -- ^ what assumes it
      (Maybe LocationInfo)
  | MetaBinderWarning
      VarIdent              -- ^ the declaration
      VarIdent              -- ^ the variable bound inside a term
      String                -- ^ its type, rendered
      (Maybe LocationInfo)
  deriving (Eq, Show)

-- | Diagnostic categories for constructs outside the RSTT fragment.
data RSTTExtension = RSTTModal | RSTTInterval | RSTTInductive | RSTTShapeDependency | RSTTUnsupported | RSTTSchematic
  deriving (Eq, Show)

-- | What assumes a free-standing restriction (see "Rzk.TypeCheck.Fragment.RSTT"),
-- which conservativity allows to be concluded but not assumed.
data FragmentUse
  = UseBinder
    -- ^ the type of a binder (λ, Π, Σ, or a declaration's parameter)
  | UseMotive
    -- ^ the motive of an eliminator
  | UseData
    -- ^ inside a type passed as data, at a meta-typed argument or component
  | UseIdentity
    -- ^ the type of an identity type, whose endpoints it types
  | UseConcluded
    -- ^ a concluded type, off the spine of codomains (a Σ component, say)
  deriving (Eq, Show)

-- | Where a warning points, for per-file attribution.
warningLocation :: CheckWarning -> Maybe LocationInfo
warningLocation (LargeInductiveTypeWarning _ _ loc)  = loc
warningLocation (MetaPrefixWarning _ _ _ _ _ loc)    = loc
warningLocation (RSTTScopeWarning _ _ loc)           = loc
warningLocation (RSTTIncompleteWarning _ loc)       = loc
warningLocation (RSTTHoleWarning loc)               = loc
warningLocation (OverhangWarning _ _ _ loc)         = loc
warningLocation (TopeFamilyDomainWarning _ _ loc)    = loc
warningLocation (FreeStandingRestrictionWarning _ _ _ loc) = loc
warningLocation (MetaBinderWarning _ _ _ loc)       = loc

-- | Which candidate rule of the meta-parameter layer check flags a
-- 'MetaPrefixWarning' (see "Rzk.TypeCheck.MetaPrefix"): the structural
-- rule, or only its stricter variant. Both are emitted so the two
-- candidate defaults can be measured on a corpus side by side.
data MetaPrefixRule
  = MetaPrefixBoth
  | MetaPrefixStrictOnly
  deriving (Eq, Show)

-- | What a run records besides its result: the holes it found and the non-fatal
-- findings it made. Both accumulate in reverse and are turned around by
-- 'checkLog' when the run ends.
data CheckLog = CheckLog
  { logHolesRev    :: [HoleInfo]
  , logWarningsRev :: [CheckWarning]
  , logSchematicCache :: IntSet.IntSet
  -- Nothing records an unsuccessful or ongoing object-family probe.
  , logSchematicObjectFamilies :: IntMap.IntMap (Maybe Int)
  }

emptyCheckLog :: CheckLog
emptyCheckLog = CheckLog [] [] IntSet.empty IntMap.empty

-- | What a run recorded, in the order it was recorded.
checkLog :: CheckLog -> ([HoleInfo], [CheckWarning])
checkLog (CheckLog holes warnings _ _) = (reverse holes, reverse warnings)

-- | The record of a run is kept in the /state/, beneath the error channel,
-- rather than on a writer channel above it.
--
-- The two differ exactly where a caught error is concerned: a writer discards
-- what the failing action wrote, and the state keeps it. That is what the
-- checker wants. A command that fails still reports the holes the user wrote in
-- it, and checking goes on to the next command with those holes in hand (see
-- @withCommand@ in "Rzk.TypeCheck.Decl"). A probe that wants the older
-- behaviour asks for it, with 'suppressing'.
type TypeCheck n =
  ReaderT (Context n)
    (ExceptT TypeErrorInScopedContext (State CheckLog))

-- | Run a judgement in a given context, keeping what it recorded.
runTypeCheckWith
  :: Context n -> TypeCheck n a
  -> (Either TypeErrorInScopedContext a, ([HoleInfo], [CheckWarning]))
runTypeCheckWith ctx tc =
  case runState (runExceptT (runReaderT tc ctx)) emptyCheckLog of
    (result, logged) -> (result, checkLog logged)

-- | Run a judgement in the empty context, discarding the holes it records.
runTypeCheck :: TypeCheck Foil.VoidS a -> Either TypeErrorInScopedContext a
runTypeCheck = runTypeCheckIn emptyContext

-- | Run a judgement in a given context, discarding the holes it records.
runTypeCheckIn :: Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
runTypeCheckIn ctx tc = fst (runTypeCheckWith ctx tc)

-- | Run a judgement in another scope's context.
--
-- The error channel and the hole channel are shared and carry no scope index, so
-- there is nothing to translate: this is 'runReaderT' with the inner scope's
-- context, lifted back. Holes recorded inside land in the same state, and an
-- error thrown inside already carries its own context.
inContext :: Context l -> TypeCheck l a -> TypeCheck n a
inContext ctx = lift . flip runReaderT ctx

-- * Errors

-- | Raise a type error, capturing the context it happened in.
issueTypeError :: Distinct n => TypeError n -> TypeCheck n a
issueTypeError err = do
  ctx <- ask
  throwError (TypeErrorInScopedContext ctx err)

issueWarning :: String -> TypeCheck n ()
issueWarning message = trace ("Warning: " <> message) (return ())

-- * Tracing

trace' :: Verbosity -> Verbosity -> String -> a -> a
trace' Silent _ _ = id
trace' Normal Debug _ = id
trace' _ _ msg = trace msg

traceTypeCheck :: Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck verbosity msg action = do
  configuredVerbosity <- asks ctxVerbosity
  trace' configuredVerbosity verbosity msg action

localVerbosity :: Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity verbosity = local $ \ctx -> ctx { ctxVerbosity = verbosity }

localRenderBackend :: Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend backend = local $ \ctx -> ctx { ctxRenderBackend = backend }

localHideTerm :: Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm hide = local $ \ctx -> ctx { ctxRenderHideTerm = hide }

localWarnOverhang :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang warn = local $ \ctx -> ctx { ctxWarnOverhang = warn }

localWarnTopeFamilyDomain :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnTopeFamilyDomain warn = local $ \ctx -> ctx { ctxWarnTopeFamilyDomain = warn }

localWarnFreeStandingRestriction :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnFreeStandingRestriction warn =
  local $ \ctx -> ctx { ctxStandaloneWarnFreeStandingRestriction = warn }

localWarnShapeDependency :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnShapeDependency warn = local $ \ctx -> ctx { ctxStandaloneWarnShapeDependency = warn }

localWarnMetaBinder :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnMetaBinder warn = local $ \ctx -> ctx { ctxStandaloneWarnMetaBinder = warn }

localMetaPrefixSensitivity :: MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity sensitivity =
  local $ \ctx -> ctx { ctxMetaPrefixSensitivity = sensitivity }

-- | Render the enclosed action with the proof term hidden.
hidingTerm :: TypeCheck n a -> TypeCheck n a
hidingTerm = localHideTerm True

-- * Variance

switchVariance :: TypeCheck n a -> TypeCheck n a
switchVariance = local $ \ctx -> ctx { ctxCovariance = switch (ctxCovariance ctx) }
  where
    switch Covariant     = Contravariant
    switch Contravariant = Covariant
    switch Invariant     = Invariant

setVariance :: Covariance -> TypeCheck n a -> TypeCheck n a
setVariance variance = local $ \ctx -> ctx { ctxCovariance = variance }

-- * The judgement stack

-- | The depth of nested judgements at which type checking gives up. Well-typed
-- input stays far below it; the cap catches a non-terminating search.
-- FIXME: expose as a parameter (@--max-depth@ and @rzk.yaml@).
maxActionStackDepth :: Int
maxActionStackDepth = 1000

performing :: Distinct n => Action n -> TypeCheck n a -> TypeCheck n a
performing action tc = do
  ctx@Context{..} <- ask
  unless (ctxActionStackDepth < maxActionStackDepth) $
    issueTypeError $ TypeErrorOther "maximum depth reached"
  let ctx' = ctx
        { ctxActionStack = action : ctxActionStack
        , ctxActionStackDepth = ctxActionStackDepth + 1
        , ctxLocation = narrowLocation action ctxLocation
        }
  -- The trace message is built only when it is actually printed: at normal
  -- verbosity rendering the action's terms on every judgement would cost a
  -- thunk per judgement.
  if ctxVerbosity <= Debug
    then trace (ppAction (namingOfContext ctx) ctxActionStackDepth action) $
           local (const ctx') tc
    else local (const ctx') tc

-- | Point the location at the sub-term an action is about.
--
-- The checker descends through 'performing', so the location narrows as it
-- goes and an error is reported where the sub-term that caused it was written,
-- rather than at the declaration it is in (issue #81). A judgement about a term
-- the checker built itself carries no position, and leaves the location as it
-- found it: that is the innermost enclosing term the user did write.
narrowLocation :: Action n -> Maybe LocationInfo -> Maybe LocationInfo
narrowLocation action loc = case termOf action of
  Just term | Just pos <- positionOfTerm term -> atPosition pos <$> loc
  _                                           -> loc
  where
    termOf (ActionTypeCheck term _) = Just term
    termOf (ActionInfer term)       = Just term
    termOf _                        = Nothing

-- * What a run records

modifyLog :: (CheckLog -> CheckLog) -> TypeCheck n ()
modifyLog f = lift (lift (modify' f))

-- | Run a probe for its answer alone, discarding whatever it records.
--
-- A hole's inventory is built by trying candidate moves and seeing which fit,
-- and each trial checks terms of its own; their holes and warnings are not the
-- user's and must not reach the report. This is what the writer channel's
-- @censor@ did before the record moved into the state: the state survives an
-- error, so it is put back on that path too.
suppressing :: TypeCheck n a -> TypeCheck n a
suppressing action = do
  saved <- lift (lift get)
  let restore = lift (lift (put saved))
  result <- action `catchError` \err -> restore >> throwError err
  restore
  return result

-- * Holes

recordHoleInfo :: Distinct n => HoleInfo -> TypeCheck n ()
recordHoleInfo info = do
  modifyLog $ \l -> l { logHolesRev = info : logHolesRev l }
  enabled <- asks rsttSafeEnabled
  when enabled $ recordCheckWarning (RSTTHoleWarning (holeLocation info))

-- * Warnings

-- | Record a warning once, rejecting fragment violations in safe error mode.
recordCheckWarning :: Distinct n => CheckWarning -> TypeCheck n ()
recordCheckWarning warning = do
  -- Signature and body elaboration may report the same annotation twice.
  modifyLog $ \l ->
    if warning `elem` logWarningsRev l then l
    else l { logWarningsRev = warning : logWarningsRev l }
  mode <- asks rsttSafeMode
  when (mode == RSTTSafeError) $
    mapM_ (issueTypeError . TypeErrorRSTT) (rsttViolation warning)

-- | Describe a fragment violation; return 'Nothing' for unrelated warnings.
rsttViolation :: CheckWarning -> Maybe String
rsttViolation = \case
  MetaPrefixWarning _ _ _ _ _ _ -> Just "unsaturated schematic parameters"
  FreeStandingRestrictionWarning _ _ _ _ -> Just "free-standing restriction in an assumed position"
  MetaBinderWarning _ _ _ _ -> Just "schematic binder inside a term"
  RSTTScopeWarning _ feature _ -> Just (feature <> " is outside RSTT")
  RSTTHoleWarning _ -> Just "unfinished obligation"
  RSTTIncompleteWarning reason _ -> Just reason
  _ -> Nothing

-- | Report an unfinished fragment check without masking a safe-mode error.
reportIncompleteRSTTCheck :: Distinct n => String -> TypeErrorInScopedContext -> TypeCheck n ()
reportIncompleteRSTTCheck _ err@(TypeErrorInScopedContext _ TypeErrorRSTT{}) = throwError err
reportIncompleteRSTTCheck what (TypeErrorInScopedContext _ err) = do
  loc <- asks ctxLocation
  let reason = case err of
        TypeErrorOther message -> message
        _ -> "could not inspect a type"
  recordCheckWarning $ RSTTIncompleteWarning (what <> ": " <> reason) loc

-- * Locations

withLocation :: LocationInfo -> TypeCheck n a -> TypeCheck n a
withLocation loc = local $ \ctx -> ctx { ctxLocation = Just loc }