{-# LANGUAGE GADTs #-}

-- | Subsumption checking
module Language.PureScript.TypeChecker.Subsumption
  ( subsumes
  ) where

import Prelude

import Control.Monad (when)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..))

import Data.Foldable (for_)
import Data.List (uncons)
import Data.List.Ordered (minusBy')
import Data.Ord (comparing)

import Language.PureScript.AST (ErrorMessageHint(..), Expr(..), pattern NullSourceAnn)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (tyFunction, tyRecord)
import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), errorMessage, internalCompilerError)
import Language.PureScript.TypeChecker.Monad (CheckState, getHints, getTypeClassDictionaries, withErrorMessageHint)
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize)
import Language.PureScript.TypeChecker.Unify (alignRowsWith, freshTypeWithKind, unifyTypes)
import Language.PureScript.Types (RowListItem(..), SourceType, Type(..), eqType, isREmpty, replaceTypeVars, rowFromList)

-- | Subsumption can operate in two modes:
--
-- * Elaboration mode, in which we try to insert type class dictionaries
-- * No-elaboration mode, in which we do not insert dictionaries
--
-- Some subsumption rules apply in both modes, and others are specific to
-- certain modes.
--
-- The subsumption algorithm follows the structure of the types in question,
-- and we can switch into no-elaboration mode when we move under a type
-- constructor where we can no longer insert dictionaries, e.g. into the fields
-- of a record.
data Mode = Elaborate | NoElaborate

-- | Value-level proxies for the two modes
data ModeSing (mode :: Mode) where
  SElaborate   :: ModeSing 'Elaborate
  SNoElaborate :: ModeSing 'NoElaborate

-- | This type family tracks what evidence we return from 'subsumes' for each
-- mode.
type family Coercion (mode :: Mode) where
  -- When elaborating, we generate a coercion
  Coercion 'Elaborate = Expr -> Expr
  -- When we're not elaborating, we don't generate coercions
  Coercion 'NoElaborate = ()

-- | The default coercion for each mode.
defaultCoercion :: ModeSing mode -> Coercion mode
defaultCoercion SElaborate   = id
defaultCoercion SNoElaborate = ()

-- | Check that one type subsumes another, rethrowing errors to provide a better error message
subsumes
  :: (MonadError MultipleErrors m, MonadState CheckState m)
  => SourceType
  -> SourceType
  -> m (Expr -> Expr)
subsumes ty1 ty2 =
  withErrorMessageHint (ErrorInSubsumption ty1 ty2) $
    subsumes' SElaborate ty1 ty2

-- | Check that one type subsumes another
subsumes'
  :: (MonadError MultipleErrors m, MonadState CheckState m)
  => ModeSing mode
  -> SourceType
  -> SourceType
  -> m (Coercion mode)
subsumes' mode (ForAll _ _ ident mbK ty1 _) ty2 = do
  u <- maybe (internalCompilerError "Unelaborated forall") freshTypeWithKind mbK
  let replaced = replaceTypeVars ident u ty1
  subsumes' mode replaced ty2
subsumes' mode ty1 (ForAll _ _ ident mbK ty2 sco) =
  case sco of
    Just sco' -> do
      sko <- newSkolemConstant
      let sk = skolemize NullSourceAnn ident mbK sko sco' ty2
      subsumes' mode ty1 sk
    Nothing -> internalError "subsumes: unspecified skolem scope"
subsumes' mode (TypeApp _ (TypeApp _ f1 arg1) ret1) (TypeApp _ (TypeApp _ f2 arg2) ret2) | eqType f1 tyFunction && eqType f2 tyFunction = do
  subsumes' SNoElaborate arg2 arg1
  subsumes' SNoElaborate ret1 ret2
  -- Nothing was elaborated, return the default coercion
  return (defaultCoercion mode)
subsumes' mode (KindedType _ ty1 _) ty2 =
  subsumes' mode ty1 ty2
subsumes' mode ty1 (KindedType _ ty2 _) =
  subsumes' mode ty1 ty2
-- Only check subsumption for constrained types when elaborating.
-- Otherwise fall back to unification.
subsumes' SElaborate (ConstrainedType _ con ty1) ty2 = do
  dicts <- getTypeClassDictionaries
  hints <- getHints
  elaborate <- subsumes' SElaborate ty1 ty2
  let addDicts val = App val (TypeClassDictionary con dicts hints)
  return (elaborate . addDicts)
subsumes' mode (TypeApp _ f1 r1) (TypeApp _ f2 r2) | eqType f1 tyRecord && eqType f2 tyRecord = do
    let goWithLabel l t1 t2 = withErrorMessageHint (ErrorInRowLabel l) $ subsumes' SNoElaborate t1 t2
    let (common, ((ts1', r1'), (ts2', r2'))) = alignRowsWith goWithLabel r1 r2
    -- For { ts1 | r1 } to subsume { ts2 | r2 } when r1 is empty (= we're working with a closed row),
    -- every property in ts2 must appear in ts1. If not, then the candidate expression is missing a required property.
    -- Conversely, when r2 is empty, every property in ts1 must appear in ts2, or else the expression has
    -- an additional property which is not allowed.
    when (isREmpty r1')
      (for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . rowListLabel))
    when (isREmpty r2')
      (for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . rowListLabel))
    -- Check subsumption for common labels
    sequence_ common
    -- Inject the info here
    unifyTypes (rowFromList (ts1', r1')) (rowFromList (ts2', r2'))
    -- Nothing was elaborated, return the default coercion
    return (defaultCoercion mode)
  where
    -- Find the first property that's in the first list (of tuples) but not in the second
    firstMissingProp t1 t2 = fst <$> uncons (minusBy' (comparing rowListLabel) t1 t2)
subsumes' mode ty1 ty2@(TypeApp _ obj _) | obj == tyRecord =
  subsumes' mode ty2 ty1
subsumes' mode ty1 ty2 = do
  unifyTypes ty1 ty2
  -- Nothing was elaborated, return the default coercion
  return (defaultCoercion mode)