{-# LANGUAGE
    ViewPatterns
  , OverloadedStrings
  , NamedFieldPuns
  , LambdaCase
  , TupleSections
  , RecordWildCards
  , MultiWayIf
  , TypeApplications
  , OverloadedRecordDot
  , ScopedTypeVariables
#-}

{-# OPTIONS_GHC -Wno-unused-local-binds #-}

module Control.Monad.CheckedExcept.Plugin.Bind
  ( bindPlugin
  -- disable unused warnings
  , tcPrintLn
  , tcPrint
  , tcPrintOutputable
  , tcTraceLabel
  , evByFiat
  )
where

import GHC.Plugins hiding ((<>))
import GHC.Tc.Types.Constraint
import qualified GHC.Tc.Plugin as TC
import qualified GHC.Tc.Types as TC
import GHC.Tc.Types.Evidence (EvTerm (..), evCast)
import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
import GHC.Tc.Plugin (tcPluginTrace)
import Data.List (nubBy)
import GHC.Types.Unique (hasKey)
import GHC.Builtin.Names (consDataConKey)
import Data.Maybe (mapMaybe, listToMaybe)
import Data.Bifunctor (second)
import GHC.Core.Reduction (Reduction(..))
import GHC.Tc.Utils.TcType (eqType)
import Control.Monad (join)

{-
    ************************************************************
    *                                                          *
    *                  Plugin initialization                   *
    *                                                          *
    ************************************************************
-}

data Environment = Environment
  { Environment -> TyCon
containsTyCon :: TyCon
  , Environment -> TyCon
elem'TyCon :: TyCon
  , Environment -> TyCon
elemTyCon :: TyCon
  , Environment -> TyCon
checkedExceptTTyCon :: TyCon
  , Environment -> TyCon
notElemTypeErrorTyCon :: TyCon
  }

bindPlugin :: TcPlugin
bindPlugin :: TcPlugin
bindPlugin [CommandLineOption]
_ = TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just (TcPlugin -> Maybe TcPlugin) -> TcPlugin -> Maybe TcPlugin
forall a b. (a -> b) -> a -> b
$ TC.TcPlugin
  { tcPluginInit :: TcPluginM Environment
TC.tcPluginInit = do
      checkedExceptMod <- TcPluginM Module
lookupCheckedExceptMod
      containsTyCon <- lookupContains checkedExceptMod
      elem'TyCon <- lookupElem' checkedExceptMod
      elemTyCon <- lookupElem checkedExceptMod
      checkedExceptTTyCon <- lookupCheckedExceptT checkedExceptMod
      notElemTypeErrorTyCon <- lookupNotElemTypeError checkedExceptMod
      pure Environment {..}
  , tcPluginSolve :: Environment -> TcPluginSolver
TC.tcPluginSolve = Environment -> TcPluginSolver
solveBind
  , tcPluginStop :: Environment -> TcPluginM ()
TC.tcPluginStop = TcPluginM () -> Environment -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM () -> Environment -> TcPluginM ())
-> TcPluginM () -> Environment -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , tcPluginRewrite :: Environment -> UniqFM TyCon TcPluginRewriter
TC.tcPluginRewrite = Environment -> UniqFM TyCon TcPluginRewriter
mkRewriter
  }

lookupTyConWithMod :: String -> Module -> TC.TcPluginM TyCon
lookupTyConWithMod :: CommandLineOption -> Module -> TcPluginM TyCon
lookupTyConWithMod CommandLineOption
name Module
modCE = do
  let tyCo_OccName :: OccName
tyCo_OccName = CommandLineOption -> OccName
mkTcOcc CommandLineOption
name
  tyCo <- Module -> OccName -> TcPluginM Name
TC.lookupOrig Module
modCE OccName
tyCo_OccName
  TC.tcLookupTyCon tyCo

lookupCheckedExceptMod :: TC.TcPluginM Module
lookupCheckedExceptMod :: TcPluginM Module
lookupCheckedExceptMod = do
   findResult <- ModuleName -> PkgQual -> TcPluginM FindResult
TC.findImportedModule ( CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"Control.Monad.CheckedExcept" ) PkgQual
NoPkgQual -- ( Just "checked-exceptions" )
   case findResult of
     TC.Found ModLocation
_ Module
modCE -> Module -> TcPluginM Module
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Module
modCE
     FindResult
_ -> CommandLineOption -> TcPluginM Module
forall a. HasCallStack => CommandLineOption -> a
error CommandLineOption
"Couldn't find Control.Monad.CheckedExcept"

lookupContains :: Module -> TC.TcPluginM TyCon
lookupContains :: Module -> TcPluginM TyCon
lookupContains = CommandLineOption -> Module -> TcPluginM TyCon
lookupTyConWithMod CommandLineOption
"Contains"

lookupElem' :: Module -> TC.TcPluginM TyCon
lookupElem' :: Module -> TcPluginM TyCon
lookupElem' = CommandLineOption -> Module -> TcPluginM TyCon
lookupTyConWithMod CommandLineOption
"Elem'"

lookupElem :: Module -> TC.TcPluginM TyCon
lookupElem :: Module -> TcPluginM TyCon
lookupElem = CommandLineOption -> Module -> TcPluginM TyCon
lookupTyConWithMod CommandLineOption
"Elem"

lookupCheckedExceptT :: Module -> TC.TcPluginM TyCon
lookupCheckedExceptT :: Module -> TcPluginM TyCon
lookupCheckedExceptT Module
modCE = do
  let
    myTyFam_OccName :: OccName
    myTyFam_OccName :: OccName
myTyFam_OccName = CommandLineOption -> OccName
mkTcOcc CommandLineOption
"CheckedExceptT"
  myTyFam_Name <- Module -> OccName -> TcPluginM Name
TC.lookupOrig Module
modCE OccName
myTyFam_OccName
  TC.tcLookupTyCon myTyFam_Name

lookupNotElemTypeError :: Module -> TC.TcPluginM TyCon
lookupNotElemTypeError :: Module -> TcPluginM TyCon
lookupNotElemTypeError = CommandLineOption -> Module -> TcPluginM TyCon
lookupTyConWithMod CommandLineOption
"NotElemTypeError"

{-
    ************************************************************
    *                                                          *
    *     Control.Monad.CheckedExcept constraint solver        *
    *                                                          *
    ************************************************************
-}

solveBind :: Environment -> TC.TcPluginSolver
solveBind :: Environment -> TcPluginSolver
solveBind Environment
_ EvBindsVar
_ [Ct]
_ [] = TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TC.TcPluginOk [] []
solveBind env :: Environment
env@Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} EvBindsVar
_evBinds [Ct]
_givens [Ct]
wanteds = do
  (solved, insoluable, newCt) <- [([(EvTerm, Ct)], [Ct], [Ct])] -> ([(EvTerm, Ct)], [Ct], [Ct])
forall a b c. [([a], [b], [c])] -> ([a], [b], [c])
concatUnzip3 ([([(EvTerm, Ct)], [Ct], [Ct])] -> ([(EvTerm, Ct)], [Ct], [Ct]))
-> TcPluginM [([(EvTerm, Ct)], [Ct], [Ct])]
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct]))
-> [Ct] -> TcPluginM [([(EvTerm, Ct)], [Ct], [Ct])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Ct -> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
solve1Wanted [Ct]
wanteds
  pure TC.TcPluginSolveResult
    { tcPluginInsolubleCts = insoluable
    , tcPluginSolvedCts = solved
    , tcPluginNewCts = newCt
    }
  where
  solve1Wanted ::
       Ct
    -> TC.TcPluginM
          ( [(EvTerm, Ct)] -- solved
          , [Ct] -- unsolved
          , [Ct] -- new work
          )
  solve1Wanted :: Ct -> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
solve1Wanted Ct
unzonkedWanted =
    Ct -> TcPluginM Ct
TC.zonkCt Ct
unzonkedWanted TcPluginM Ct
-> (Ct -> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct]))
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Ct
wanted ->
      let noNewWork :: p -> p -> Bool
noNewWork p
_ p
_ = Bool
False
          yesNewWork :: p -> p -> Bool
yesNewWork p
_ p
_ = Bool
True

          -- not quite right, since we do substitutions...
          newWorkIfVar :: Type -> Type -> Bool
newWorkIfVar Type
ty1 Type
ty2 = Bool -> Bool
not (Type -> Bool
isUnified Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isUnified Type
ty2)

          defWork :: p -> p -> Bool
defWork = p -> p -> Bool
forall {p} {p}. p -> p -> Bool
yesNewWork

          transformConstraint :: CommandLineOption
-> CtEvidence
-> a
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [a], [Ct])
transformConstraint CommandLineOption
label CtEvidence
ir_ev a
ir_reason Type
ty1Unzonked Type
ty2Unzonked Type -> Type -> Bool
hasNewWork Type -> Type -> Type
mkNewPred = do
            CommandLineOption -> CtEvidence -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel (CommandLineOption
label CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
"_ir_ev") CtEvidence
ir_ev
            CommandLineOption -> a -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel (CommandLineOption
label CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
"_ir_reason") a
ir_reason
            mtys <- Environment -> Ct -> Type -> Type -> TcPluginM (Maybe (Type, Type))
disambiguateTypeVarsUsingReturnType Environment
env Ct
wanted Type
ty1Unzonked Type
ty2Unzonked
            let mkNewWanted Type
ty1 Type
ty2 Type
newPred = do
                  if Type -> Type -> Bool
hasNewWork Type
ty1 Type
ty2
                  then CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> TcPluginM CtEvidence -> TcPluginM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Type -> TcPluginM CtEvidence
TC.newWanted (Ct -> CtLoc
ctLoc Ct
wanted) Type
newPred
                  else Ct -> TcPluginM Ct
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ct -> TcPluginM Ct) -> Ct -> TcPluginM Ct
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical (HasDebugCallStack => CtEvidence -> Type -> CtEvidence
CtEvidence -> Type -> CtEvidence
setCtEvPredType CtEvidence
ir_ev (Type -> CtEvidence) -> Type -> CtEvidence
forall a b. (a -> b) -> a -> b
$ Type
newPred)
            case mtys of
              Maybe (Type, Type)
Nothing -> do
                ([(EvTerm, Ct)], [a], [Ct])
-> TcPluginM ([(EvTerm, Ct)], [a], [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(EvTerm, Ct)], [a], [Ct])
forall a. Monoid a => a
mempty -- catch this in the rewriter
              Just (Type
ty1, Type
ty2) -> do
                let newPred :: Type
newPred = [(Type, Type)] -> Type -> Type
substituteTypeVars [(Type
ty1Unzonked, Type
ty1), (Type
ty2Unzonked, Type
ty2)] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
mkNewPred Type
ty1 Type
ty2
                newWanted <- Type -> Type -> Type -> TcPluginM Ct
mkNewWanted Type
ty1 Type
ty2 Type
newPred
                pure
                  ( [ ( trustMeBro ("checked-exceptions:" <> label <> ":ambiguous") (ctEvExpr $ ctEvidence newWanted) (ctPred newWanted) (ctPred wanted)
                       , wanted
                       )
                    ]
                  , []
                  , if hasNewWork ty1 ty2 then [newWanted] else []
                  )
      in
      case Ct
wanted of
        CIrredCan (IrredCt {ir_ev :: IrredCt -> CtEvidence
ir_ev = ir_ev :: CtEvidence
ir_ev@CtWanted{Type
CtLoc
RewriterSet
TcEvDest
ctev_pred :: Type
ctev_dest :: TcEvDest
ctev_loc :: CtLoc
ctev_rewriters :: RewriterSet
ctev_loc :: CtEvidence -> CtLoc
ctev_pred :: CtEvidence -> Type
ctev_rewriters :: CtEvidence -> RewriterSet
ctev_dest :: CtEvidence -> TcEvDest
..}, CtIrredReason
ir_reason :: CtIrredReason
ir_reason :: IrredCt -> CtIrredReason
ir_reason}) -> do
          if
            -- Check if it's `Contains`
            | Just (TyCon
tc, [Type
tk], [Type
ty1Unzonked, Type
ty2Unzonked]) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
ctev_pred
            , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
containsTyCon
            -> CommandLineOption
-> CtEvidence
-> CtIrredReason
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall {a} {a}.
Outputable a =>
CommandLineOption
-> CtEvidence
-> a
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [a], [Ct])
transformConstraint CommandLineOption
"contains" CtEvidence
ir_ev CtIrredReason
ir_reason Type
ty1Unzonked Type
ty2Unzonked Type -> Type -> Bool
forall {p} {p}. p -> p -> Bool
defWork (\Type
ty1 Type
ty2 -> Environment -> Type -> Type -> Type -> Type -> Type
substContains Environment
env Type
tk Type
ty1 Type
ty2 Type
ctev_pred)

            -- Check if it's `If (Elem'`
            | Just (TyCon
tcIf, [Type]
_, [Type
elemTf, Type
_, Type
_]) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
ctev_pred
            , TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tcIf OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== CommandLineOption -> OccName
mkTcOcc CommandLineOption
"If"
            , Just (TyCon
tcElem', [Type]
_, [Type
ty1Unzonked, Type
ty2Unzonked]) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
elemTf
            , TyCon
tcElem' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
elem'TyCon
            -> do CommandLineOption
-> CtEvidence
-> CtIrredReason
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall {a} {a}.
Outputable a =>
CommandLineOption
-> CtEvidence
-> a
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [a], [Ct])
transformConstraint CommandLineOption
"if_1" CtEvidence
ir_ev CtIrredReason
ir_reason Type
ty1Unzonked Type
ty2Unzonked Type -> Type -> Bool
forall {p} {p}. p -> p -> Bool
defWork (\Type
ty1 Type
ty2 -> Environment -> Type -> Type -> Type -> Type
substElem' Environment
env Type
ty1 Type
ty2 Type
ctev_pred)

            -- Check if it's `Elem`
            | Just (TyCon
tcElem, [Type]
_, [Type
ty1Unzonked, Type
ty2Unzonked]) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
ctev_pred
            , TyCon
tcElem TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
elemTyCon
            -> do CommandLineOption
-> CtEvidence
-> CtIrredReason
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall {a} {a}.
Outputable a =>
CommandLineOption
-> CtEvidence
-> a
-> Type
-> Type
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> TcPluginM ([(EvTerm, Ct)], [a], [Ct])
transformConstraint CommandLineOption
"elem_2" CtEvidence
ir_ev CtIrredReason
ir_reason Type
ty1Unzonked Type
ty2Unzonked Type -> Type -> Bool
forall {p} {p}. p -> p -> Bool
defWork (\Type
ty1 Type
ty2 -> Environment -> Type -> Type -> Type -> Type
substElem Environment
env Type
ty1 Type
ty2 Type
ctev_pred)

            | Bool
otherwise -> do
                CommandLineOption -> (FastString, Ct) -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"unwanted2" (Ct -> FastString
ctKind Ct
wanted, Ct
wanted)
                ([(EvTerm, Ct)], [Ct], [Ct])
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [Ct
wanted], [])

        Ct
_ -> do
          CommandLineOption -> (FastString, Ct) -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"unwanted" (Ct -> FastString
ctKind Ct
wanted, Ct
wanted)
          ([(EvTerm, Ct)], [Ct], [Ct])
-> TcPluginM ([(EvTerm, Ct)], [Ct], [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [Ct
wanted], [])

substContains :: Environment -> Type -> Type -> Type -> PredType -> PredType
substContains :: Environment -> Type -> Type -> Type -> Type -> Type
substContains Environment
_env Type
_tk Type
ty1 Type
_ty2 Type
predTy =
  case Type -> Maybe CoreBndr
getTyVar_maybe Type
ty1 of
    Maybe CoreBndr
Nothing -> Type
predTy
    Just CoreBndr
ty1Var -> [CoreBndr] -> [Type] -> Type -> Type
HasDebugCallStack => [CoreBndr] -> [Type] -> Type -> Type
substTyWith [CoreBndr
ty1Var] [Type
emptyListKindTy] Type
predTy

substElem' :: Environment -> Type -> Type -> PredType -> PredType
substElem' :: Environment -> Type -> Type -> Type -> Type
substElem' Environment
_env Type
_ty1 Type
ty2 Type
predTy =
  case Type -> Maybe CoreBndr
getTyVar_maybe Type
ty2 of
    Maybe CoreBndr
Nothing -> Type
predTy
    Just CoreBndr
ty2Var -> [CoreBndr] -> [Type] -> Type -> Type
HasDebugCallStack => [CoreBndr] -> [Type] -> Type -> Type
substTyWith [CoreBndr
ty2Var] [Type
emptyListKindTy] Type
predTy

substElem :: Environment -> Type -> Type -> PredType -> PredType
substElem :: Environment -> Type -> Type -> Type -> Type
substElem Environment
_env Type
_ty1 Type
ty2 Type
predTy =
  case Type -> Maybe CoreBndr
getTyVar_maybe Type
ty2 of
    Maybe CoreBndr
Nothing -> Type
predTy
    Just CoreBndr
ty2Var -> [CoreBndr] -> [Type] -> Type -> Type
HasDebugCallStack => [CoreBndr] -> [Type] -> Type -> Type
substTyWith [CoreBndr
ty2Var] [Type
emptyListKindTy] Type
predTy

-- Function to disambiguate type variables using the return type of the function from which the wanted constraint arises
disambiguateTypeVarsUsingReturnType :: Environment -> Ct -> Type -> Type -> TC.TcPluginM (Maybe (Type, Type))
disambiguateTypeVarsUsingReturnType :: Environment -> Ct -> Type -> Type -> TcPluginM (Maybe (Type, Type))
disambiguateTypeVarsUsingReturnType Environment {TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} Ct
wanted Type
ty1 Type
ty2 = do
  fnType <- CtLocEnv -> TcPluginM (Type, Arity)
lookupReturnType (CtLoc -> CtLocEnv
ctLocEnv (Ct -> CtLoc
ctLoc Ct
wanted))
  tcTraceLabel "fnType" fnType
  esType <- do
      let fnTyArgs = (Type, Arity) -> [(Scaled Type, Maybe FunTyFlag)]
getRuntimeArgTysOrTy (Type, Arity)
fnType
          mts = case [(Scaled Type, Maybe FunTyFlag)]
-> Maybe (Scaled Type, Maybe FunTyFlag)
forall a. [a] -> Maybe a
lastMaybe [(Scaled Type, Maybe FunTyFlag)]
fnTyArgs of
                Just (Scaled Type
st,Maybe FunTyFlag
_) -> do
                  ts1 <- TyCon -> Type -> Maybe [Type]
findTyArgs TyCon
checkedExceptTTyCon (Scaled Type -> Type
forall a. Scaled a -> a
irrelevantMult Scaled Type
st)
                  esType <- case ts1 of
                    [Type
esType, Type
_, Type
_] -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
esType
                    [Type]
_ -> Maybe Type
forall a. Maybe a
Nothing
                  extractMPromotedList esType
                Maybe (Scaled Type, Maybe FunTyFlag)
Nothing -> Maybe [Type]
forall a. Maybe a
Nothing
      case mts of
        Just [Type]
ts ->  [Type] -> Type
uniquePromotedList ([Type] -> Type) -> TcPluginM [Type] -> TcPluginM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> TcPluginM Type) -> [Type] -> TcPluginM [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Type -> TcPluginM Type
TC.zonkTcType [Type]
ts
        Maybe [Type]
Nothing -> do

          let ts1 :: Maybe [Type]
ts1 = case [(Scaled Type, Maybe FunTyFlag)]
-> Maybe (Scaled Type, Maybe FunTyFlag)
forall a. [a] -> Maybe a
lastMaybe [(Scaled Type, Maybe FunTyFlag)]
fnTyArgs of
                Just (Scaled Type
st,Maybe FunTyFlag
_) -> do
                  TyCon -> Type -> Maybe [Type]
findTyArgs TyCon
checkedExceptTTyCon (Scaled Type -> Type
forall a. Scaled a -> a
irrelevantMult Scaled Type
st)
                Maybe (Scaled Type, Maybe FunTyFlag)
Nothing -> Maybe [Type]
forall a. Maybe a
Nothing
          CommandLineOption
-> [(Scaled Type, Maybe FunTyFlag)] -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"fnTyArgs" [(Scaled Type, Maybe FunTyFlag)]
fnTyArgs
          CommandLineOption -> Maybe [Type] -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"ts1" Maybe [Type]
ts1
          CommandLineOption -> TcPluginM Type
forall x. CommandLineOption -> TcPluginM x
failWithTrace CommandLineOption
"impossibru"
  tcTraceLabel "esType" esType
  if isUnified ty1 && isUnified ty2
  then pure Nothing
  else do
    zonkedTy1 <- TC.zonkTcType ty1
    zonkedTy2 <- TC.zonkTcType ty2
    let disambiguatedTy1 = if Type -> Bool
isUnified Type
zonkedTy1 then Type
zonkedTy1 else Type
esType
        disambiguatedTy2 = if Type -> Bool
isUnified Type
zonkedTy2 then Type
zonkedTy2 else Type
esType
    tcTraceLabel "ambiguous    " (ty1, ty2)
    tcTraceLabel "disambiguated" (disambiguatedTy1, disambiguatedTy2)
    pure $ Just (disambiguatedTy1, disambiguatedTy2)

-- Function to lookup the return type from the environment
lookupReturnType :: CtLocEnv -> TC.TcPluginM (Type, Arity)
lookupReturnType :: CtLocEnv -> TcPluginM (Type, Arity)
lookupReturnType CtLocEnv
env = case CtLocEnv -> TcBinderStack
ctl_bndrs CtLocEnv
env of
  ts :: TcBinderStack
ts@(TC.TcIdBndr CoreBndr
tcid TopLevelFlag
_:TcBinderStack
_) -> do
      CommandLineOption -> TcBinderStack -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"lookupReturnType" TcBinderStack
ts
      (Type, Arity) -> TcPluginM (Type, Arity)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type, Arity) -> TcPluginM (Type, Arity))
-> (Type, Arity) -> TcPluginM (Type, Arity)
forall a b. (a -> b) -> a -> b
$ (CoreBndr -> Type
idType CoreBndr
tcid, CoreBndr -> Arity
idArity CoreBndr
tcid)
  [] -> CommandLineOption -> TcPluginM (Type, Arity)
forall x. CommandLineOption -> TcPluginM x
failWithTrace CommandLineOption
"No return type found in environment"
  TcBinderStack
_ -> CommandLineOption -> TcPluginM (Type, Arity)
forall x. CommandLineOption -> TcPluginM x
failWithTrace CommandLineOption
"Unresolved return type"

{-
    ************************************************************
    *                                                          *
    *     Control.Monad.CheckedExcept type family rewriter     *
    *                                                          *
    ************************************************************
-}

mkRewriter :: Environment -> UniqFM TyCon TC.TcPluginRewriter
mkRewriter :: Environment -> UniqFM TyCon TcPluginRewriter
mkRewriter env :: Environment
env@Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} = [(TyCon, TcPluginRewriter)] -> UniqFM TyCon TcPluginRewriter
forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM 
  [ (TyCon
elem'TyCon, Environment -> TcPluginRewriter
rewriteElem' Environment
env)
  , (TyCon
elemTyCon, Environment -> TcPluginRewriter
rewriteElem Environment
env)
  , (TyCon
containsTyCon, Environment -> TcPluginRewriter
rewriteContains Environment
env)
  ]

rewriteElem' :: Environment -> TC.TcPluginRewriter
rewriteElem' :: Environment -> TcPluginRewriter
rewriteElem' env :: Environment
env@Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} = Type
-> (Type -> Type -> Type -> Type)
-> Environment
-> TcPluginRewriter
forall (f :: * -> *) p1 p2.
Applicative f =>
Type
-> (Type -> Type -> Type -> Type)
-> Environment
-> p1
-> p2
-> [Type]
-> f TcPluginRewriteResult
rewriteBothElem Type
trueCase Type -> Type -> Type -> Type
forall {p}. p -> Type -> Type -> Type
falseCase Environment
env
  where
  trueCase :: Type
trueCase = TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon []
  falseCase :: p -> Type -> Type -> Type
falseCase p
_ Type
ty1 Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
notElemTypeErrorTyCon [Type
ty1, Type
ty2]

rewriteElem :: Environment -> TC.TcPluginRewriter
rewriteElem :: Environment -> TcPluginRewriter
rewriteElem env :: Environment
env@Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} = Type
-> (Type -> Type -> Type -> Type)
-> Environment
-> TcPluginRewriter
forall (f :: * -> *) p1 p2.
Applicative f =>
Type
-> (Type -> Type -> Type -> Type)
-> Environment
-> p1
-> p2
-> [Type]
-> f TcPluginRewriteResult
rewriteBothElem Type
trueCase Type -> Type -> Type -> Type
forall {p}. p -> Type -> Type -> Type
falseCase Environment
env
  where
  trueCase :: Type
trueCase = [Type] -> Type
mkConstraintTupleTy []
  falseCase :: p -> Type -> Type -> Type
falseCase p
_tk Type
ty1 Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
notElemTypeErrorTyCon [Type
ty1, Type
ty2]

rewriteBothElem :: Applicative f => Type -> (Type -> Type -> Type -> Type) -> Environment -> p1 -> p2 -> [Type] -> f TC.TcPluginRewriteResult
rewriteBothElem :: forall (f :: * -> *) p1 p2.
Applicative f =>
Type
-> (Type -> Type -> Type -> Type)
-> Environment
-> p1
-> p2
-> [Type]
-> f TcPluginRewriteResult
rewriteBothElem Type
trueCase Type -> Type -> Type -> Type
falseCase Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} p1
_rewriteEnv p2
_givens [Type
tk, Type
ty, Type
tys] =
  case Type -> Maybe [Type]
extractMPromotedList Type
tys of
    Maybe [Type]
Nothing -> TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TC.TcPluginNoRewrite
    Just [Type]
tyList -> do
      let result :: Type
result = if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type -> Type -> Bool
eqType Type
ty) [Type]
tyList
                   then Type
trueCase
                   else Type -> Type -> Type -> Type
falseCase Type
tk Type
ty Type
tys
      let coercion :: Coercion
coercion = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"checked-exceptions") Role
Nominal (TyCon -> [Type] -> Type
mkTyConApp TyCon
elem'TyCon [Type
ty, Type
tys]) Type
result
      TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> f TcPluginRewriteResult)
-> TcPluginRewriteResult -> f TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ Reduction -> [Ct] -> TcPluginRewriteResult
TC.TcPluginRewriteTo (Coercion -> Type -> Reduction
Reduction Coercion
coercion Type
result) []
rewriteBothElem Type
_ Type -> Type -> Type -> Type
_ Environment
_ p1
_ p2
_ [Type]
_ = TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TC.TcPluginNoRewrite

rewriteContains :: Environment -> TC.TcPluginRewriter
rewriteContains :: Environment -> TcPluginRewriter
rewriteContains Environment{TyCon
containsTyCon :: Environment -> TyCon
elem'TyCon :: Environment -> TyCon
elemTyCon :: Environment -> TyCon
checkedExceptTTyCon :: Environment -> TyCon
notElemTypeErrorTyCon :: Environment -> TyCon
containsTyCon :: TyCon
elem'TyCon :: TyCon
elemTyCon :: TyCon
checkedExceptTTyCon :: TyCon
notElemTypeErrorTyCon :: TyCon
..} RewriteEnv
_rewriteEnv [Ct]
_givens [Type
tk, Type
tys1, Type
tys2] = do
  case Type -> Maybe [Type]
extractMPromotedList Type
tys1 of
    Just [Type]
tyList1 -> do
      let mkElemConstraint :: Type -> Type
mkElemConstraint Type
x = TyCon -> [Type] -> Type
mkTyConApp TyCon
elemTyCon [Type
tk, Type
x, Type
tys2]
          result :: Type
result = [Type] -> Type
mkConstraintTupleTy ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
mkElemConstraint [Type]
tyList1
      let coercion :: Coercion
coercion = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
"checked-exceptions") Role
Nominal (TyCon -> [Type] -> Type
mkTyConApp TyCon
elem'TyCon [Type
tys1, Type
tys2]) Type
result
      TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult)
-> TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ Reduction -> [Ct] -> TcPluginRewriteResult
TC.TcPluginRewriteTo (Coercion -> Type -> Reduction
Reduction Coercion
coercion Type
result) []
    Maybe [Type]
_ -> TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TC.TcPluginNoRewrite
rewriteContains Environment
_ RewriteEnv
_ [Ct]
_ [Type]
_ = do
  TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TC.TcPluginNoRewrite

{-
    ************************************************************
    *                                                          *
    *                    Utility functions                     *
    *                                                          *
    ************************************************************
-}

concatUnzip3 :: [([a],[b],[c])] -> ([a],[b],[c])
concatUnzip3 :: forall a b c. [([a], [b], [c])] -> ([a], [b], [c])
concatUnzip3 [([a], [b], [c])]
xs = ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
a, [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
b, [[c]] -> [c]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[c]]
c)
    where ([[a]]
a,[[b]]
b,[[c]]
c) = [([a], [b], [c])] -> ([[a]], [[b]], [[c]])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [([a], [b], [c])]
xs

failWithTrace :: forall x. String -> TC.TcPluginM x
failWithTrace :: forall x. CommandLineOption -> TcPluginM x
failWithTrace CommandLineOption
s = do
  CommandLineOption -> FastString -> TcPluginM ()
forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
"fail" (CommandLineOption -> FastString
mkFastString CommandLineOption
s)
  CommandLineOption -> TcPluginM x
forall x. CommandLineOption -> TcPluginM x
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail CommandLineOption
s

tcPrintLn :: String -> TC.TcPluginM ()
tcPrintLn :: CommandLineOption -> TcPluginM ()
tcPrintLn = IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
TC.tcPluginIO (IO () -> TcPluginM ())
-> (CommandLineOption -> IO ())
-> CommandLineOption
-> TcPluginM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOption -> IO ()
putStrLn

tcPrint :: String -> TC.TcPluginM ()
tcPrint :: CommandLineOption -> TcPluginM ()
tcPrint = IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
TC.tcPluginIO (IO () -> TcPluginM ())
-> (CommandLineOption -> IO ())
-> CommandLineOption
-> TcPluginM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOption -> IO ()
putStr

tcPrintOutputable :: Outputable a => a -> TC.TcPluginM ()
tcPrintOutputable :: forall a. Outputable a => a -> TcPluginM ()
tcPrintOutputable = CommandLineOption -> TcPluginM ()
tcPrintLn (CommandLineOption -> TcPluginM ())
-> (a -> CommandLineOption) -> a -> TcPluginM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption)
-> (a -> SDoc) -> a -> CommandLineOption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SDoc
forall a. Outputable a => a -> SDoc
ppr

tcTraceLabel :: Outputable a => String -> a -> TC.TcPluginM ()
tcTraceLabel :: forall a. Outputable a => CommandLineOption -> a -> TcPluginM ()
tcTraceLabel CommandLineOption
label a
x = CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace (CommandLineOption
"[checked-exceptions] " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. Semigroup a => a -> a -> a
<> CommandLineOption
label) (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x)

isUnified :: Type -> Bool
isUnified :: Type -> Bool
isUnified Type
ty =
     Type -> Bool
isTauTy Type
ty
  Bool -> Bool -> Bool
&& Type -> Bool
isConcreteType Type
ty
  Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isTyVarTy Type
ty)

emptyListKindTy :: Type
emptyListKindTy :: Type
emptyListKindTy = Type -> [Type] -> Type
mkPromotedListTy Type
tYPEKind []

uniquePromotedList :: [Type] -> Type
uniquePromotedList :: [Type] -> Type
uniquePromotedList [Type]
tys = Type -> [Type] -> Type
mkPromotedListTy Type
tYPEKind ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Bool) -> [Type] -> [Type]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Type -> Type -> Bool
eqType [Type]
tys

-- | Extract the elements of a promoted list, returns Nothing if not a promoted list
extractMPromotedList :: Type -> Maybe [Type]
extractMPromotedList :: Type -> Maybe [Type]
extractMPromotedList Type
tys = Type -> Maybe [Type]
go Type
tys
  where
    go :: Type -> Maybe [Type]
go Type
list_ty
      | Just (TyCon
tc, [Type]
_, [Type
t, Type
ts]) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
list_ty
      = Bool -> Maybe [Type] -> Maybe [Type]
forall a. HasCallStack => Bool -> a -> a
assert (TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
consDataConKey) (Maybe [Type] -> Maybe [Type]) -> Maybe [Type] -> Maybe [Type]
forall a b. (a -> b) -> a -> b
$
        case Type -> Maybe [Type]
go Type
ts of
          Maybe [Type]
Nothing -> Maybe [Type]
forall a. Maybe a
Nothing
          Just [Type]
ts' -> [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just ([Type] -> Maybe [Type]) -> [Type] -> Maybe [Type]
forall a b. (a -> b) -> a -> b
$ Type
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ts'

      | Just (TyCon
tc, [Type]
_, []) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
list_ty
      = Bool -> ([Type] -> Maybe [Type]) -> [Type] -> Maybe [Type]
forall a. HasCallStack => Bool -> a -> a
assert (TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
nilDataConKey)
        [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just []

      | Bool
otherwise
      = Maybe [Type]
forall a. Maybe a
Nothing

ctKind :: Ct -> FastString
ctKind :: Ct -> FastString
ctKind = \case
  CDictCan     {} -> FastString
"CDictCan     "
  CIrredCan    {} -> FastString
"CIrredCan    "
  CEqCan       {} -> FastString
"CEqCan       "
  CQuantCan    {} -> FastString
"CQuantCan    "
  CNonCanonical{} -> FastString
"CNonCanonical"

-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce'
evByFiat :: String -- ^ Name the coercion should have
         -> Type   -- ^ The LHS of the equivalence relation (~)
         -> Type   -- ^ The RHS of the equivalence relation (~)
         -> EvTerm
evByFiat :: CommandLineOption -> Type -> Type -> EvTerm
evByFiat CommandLineOption
name Type
t1 Type
t2 = Expr CoreBndr -> EvTerm
EvExpr (Expr CoreBndr -> EvTerm) -> Expr CoreBndr -> EvTerm
forall a b. (a -> b) -> a -> b
$ Coercion -> Expr CoreBndr
forall b. Coercion -> Expr b
Coercion (Coercion -> Expr CoreBndr) -> Coercion -> Expr CoreBndr
forall a b. (a -> b) -> a -> b
$ UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
name) Role
Nominal Type
t1 Type
t2

-- a *slightly* more safe version of evByFiat that will succeed even when
-- the new wanted's core expr is not emitted
trustMeBro :: String -- ^ Name the coercion should have
         -> Expr CoreBndr
         -> Type   -- ^ The LHS of the equivalence relation (~)
         -> Type   -- ^ The RHS of the equivalence relation (~)
         -> EvTerm
trustMeBro :: CommandLineOption -> Expr CoreBndr -> Type -> Type -> EvTerm
trustMeBro CommandLineOption
name Expr CoreBndr
expr Type
t1 Type
t2 = Expr CoreBndr -> Coercion -> EvTerm
evCast Expr CoreBndr
expr (Coercion -> EvTerm) -> Coercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (CommandLineOption -> UnivCoProvenance
PluginProv CommandLineOption
name) Role
Nominal Type
t1 Type
t2

-- accepts a map of types to substitute if they are type variables
-- and performs those substitutions on the tyUnsubbed argument
substituteTypeVars :: [(Type,Type)] -> Type -> Type
substituteTypeVars :: [(Type, Type)] -> Type -> Type
substituteTypeVars [(Type, Type)]
tyMap Type
tyUnsubbed =
  let ([CoreBndr]
tyVars,[Type]
concTys) =
        [(CoreBndr, Type)] -> ([CoreBndr], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(CoreBndr, Type)] -> ([CoreBndr], [Type]))
-> [(CoreBndr, Type)] -> ([CoreBndr], [Type])
forall a b. (a -> b) -> a -> b
$ ((Type, Type) -> Maybe (CoreBndr, Type))
-> [(Type, Type)] -> [(CoreBndr, Type)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
          (\(Type
tyVarTy,Type
tyRepl) -> do
              tyVar <- Type -> Maybe CoreBndr
getTyVar_maybe Type
tyVarTy
              pure (tyVar, tyRepl)
          )
          [(Type, Type)]
tyMap
  in [CoreBndr] -> [Type] -> Type -> Type
HasDebugCallStack => [CoreBndr] -> [Type] -> Type -> Type
substTyWith [CoreBndr]
tyVars [Type]
concTys Type
tyUnsubbed

splitTyConAppIgnoringKind :: Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind :: Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
ty = do
  (tyCon, tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  let (invisTys, visTys) = partitionInvisibleTypes tyCon tys
  pure (tyCon, invisTys, visTys)

-- getRunTimeArgTys can decompose certain types of arity 0 (like newtypes)
-- so we have to check the arity ourselves
getRuntimeArgTysOrTy :: (Type, Arity) -> [(Scaled Type, Maybe FunTyFlag)]
getRuntimeArgTysOrTy :: (Type, Arity) -> [(Scaled Type, Maybe FunTyFlag)]
getRuntimeArgTysOrTy (Type
ty, Arity
arity) = case Arity
arity of
  Arity
0 -> [(Type -> Scaled Type
forall a. a -> Scaled a
unrestricted Type
ty, Maybe FunTyFlag
forall a. Maybe a
Nothing)]
  Arity
_ -> ((Scaled Type, FunTyFlag) -> (Scaled Type, Maybe FunTyFlag))
-> [(Scaled Type, FunTyFlag)] -> [(Scaled Type, Maybe FunTyFlag)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FunTyFlag -> Maybe FunTyFlag)
-> (Scaled Type, FunTyFlag) -> (Scaled Type, Maybe FunTyFlag)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second FunTyFlag -> Maybe FunTyFlag
forall a. a -> Maybe a
Just) (Type -> [(Scaled Type, FunTyFlag)]
getRuntimeArgTys Type
ty)

findTyArgs :: TyCon -> Type -> Maybe [Type]
findTyArgs :: TyCon -> Type -> Maybe [Type]
findTyArgs TyCon
findTyCon Type
ty = do
  (tyCon, _, tys) <- Type -> Maybe (TyCon, [Type], [Type])
splitTyConAppIgnoringKind Type
ty
  if tyCon == findTyCon
  then Just tys
  else
    case instNewTyCon_maybe tyCon tys of
      Maybe (Type, Coercion)
Nothing -> Maybe (Maybe [Type]) -> Maybe [Type]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe [Type]) -> Maybe [Type])
-> Maybe (Maybe [Type]) -> Maybe [Type]
forall a b. (a -> b) -> a -> b
$ [Maybe [Type]] -> Maybe (Maybe [Type])
forall a. [a] -> Maybe a
listToMaybe ([Maybe [Type]] -> Maybe (Maybe [Type]))
-> [Maybe [Type]] -> Maybe (Maybe [Type])
forall a b. (a -> b) -> a -> b
$ (Type -> Maybe [Type]) -> [Type] -> [Maybe [Type]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon -> Type -> Maybe [Type]
findTyArgs TyCon
findTyCon) [Type]
tys
      Just (Type
ty', Coercion
_) -> TyCon -> Type -> Maybe [Type]
findTyArgs TyCon
findTyCon Type
ty'