{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-} {-# LANGUAGE TypeSynonymInstances, ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where import Data.Function (on) import FamInst as GHC.TypeLits.Presburger.Compat import FastString as GHC.TypeLits.Presburger.Compat (fsLit) import Class import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName, tracePlugin) import GhcPlugins as GHC.TypeLits.Presburger.Compat (lookupTyCon, mkTyConTy) import GhcPlugins as GHC.TypeLits.Presburger.Compat (mkTcOcc, ppr, promotedFalseDataCon) import GhcPlugins as GHC.TypeLits.Presburger.Compat (promotedTrueDataCon, text) import GhcPlugins as GHC.TypeLits.Presburger.Compat (tyConAppTyCon_maybe, typeKind) import GhcPlugins as GHC.TypeLits.Presburger.Compat (typeNatKind) import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName) import OccName as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc) import Plugins as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin) import TcEvidence as GHC.TypeLits.Presburger.Compat (EvTerm) import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps) import TcPluginM as GHC.TypeLits.Presburger.Compat (TcPluginM, tcLookupTyCon, tcPluginTrace) import TcRnMonad as GHC.TypeLits.Presburger.Compat (TcPluginResult (..)) import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..)) import TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts) import TcTypeNats as GHC.TypeLits.Presburger.Compat import TyCon as GHC.TypeLits.Presburger.Compat #if MIN_VERSION_ghc(8,4,1) import TcType (TcTyVar, TcType) #else import TcRnTypes (cc_ev, ctev_pred) import Data.Maybe import TcPluginM (zonkCt) #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 import GhcPlugins (InScopeSet, Outputable, emptyUFM) import qualified PrelNames as Old import TyCoRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) import Type as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv, emptyTCvSubst) import Type as GHC.TypeLits.Presburger.Compat (eqType, unionTCvSubst) import qualified Type as Old import TysWiredIn as GHC.TypeLits.Presburger.Compat (boolTyCon) import Unify as Old (tcUnifyTy) #else import Type as GHC.TypeLits.Presburger.Compat (TvSubst, emptyTvSubst) import Type as GHC.TypeLits.Presburger.Compat (substTy, unionTvSubst) import TypeRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) import TysWiredIn as Old (eqTyCon) import TysWiredIn as GHC.TypeLits.Presburger.Compat (promotedBoolTyCon) import Unify as GHC.TypeLits.Presburger.Compat (tcUnifyTy) #endif import Data.Generics.Twins import TcPluginM (lookupOrig) import TyCoRep () import Type as GHC.TypeLits.Presburger.Compat (splitTyConApp_maybe) import Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique) #if MIN_VERSION_ghc(8,4,1) import qualified GHC.TcPluginM.Extra as Extra #endif #if MIN_VERSION_ghc(8,8,1) import qualified TysWiredIn #endif #if MIN_VERSION_ghc(8,8,1) import TysWiredIn (eqTyConName) #else import PrelNames (eqTyConName) #endif #if MIN_VERSION_ghc(8,10,1) import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..)) import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred) import qualified Predicate as Old (classifyPredType) import Predicate as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) import Constraint as GHC.TypeLits.Presburger.Compat (Ct, ctEvidence, ctEvPred, isWanted) #else import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..)) import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred) import qualified GhcPlugins as Old (classifyPredType) import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, isWanted) import Type as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence) #endif #if MIN_VERSION_ghc(8,10,1) type PredTree = Pred #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv instance Outputable TvSubst where ppr :: TvSubst -> SDoc ppr = TCvSubst -> SDoc forall a. Outputable a => a -> SDoc ppr (TCvSubst -> SDoc) -> (TvSubst -> TCvSubst) -> TvSubst -> SDoc forall b c a. (b -> c) -> (a -> b) -> a -> c . TvSubst -> TCvSubst toTCv emptyTvSubst :: TvSubst emptyTvSubst :: TvSubst emptyTvSubst = case TCvSubst emptyTCvSubst of TCvSubst InScopeSet set TvSubstEnv tvsenv CvSubstEnv _ -> InScopeSet -> TvSubstEnv -> TvSubst TvSubst InScopeSet set TvSubstEnv tvsenv toTCv :: TvSubst -> TCvSubst toTCv :: TvSubst -> TCvSubst toTCv (TvSubst InScopeSet set TvSubstEnv tvenv) = InScopeSet -> TvSubstEnv -> CvSubstEnv -> TCvSubst TCvSubst InScopeSet set TvSubstEnv tvenv CvSubstEnv forall elt. UniqFM elt emptyUFM substTy :: TvSubst -> Type -> Type substTy :: TvSubst -> Type -> Type substTy TvSubst tvs = HasCallStack => TCvSubst -> Type -> Type TCvSubst -> Type -> Type Old.substTy (TvSubst -> TCvSubst toTCv TvSubst tvs) unionTvSubst :: TvSubst -> TvSubst -> TvSubst unionTvSubst :: TvSubst -> TvSubst -> TvSubst unionTvSubst TvSubst s1 TvSubst s2 = TCvSubst -> TvSubst fromTCv (TCvSubst -> TvSubst) -> TCvSubst -> TvSubst forall a b. (a -> b) -> a -> b $ TCvSubst -> TCvSubst -> TCvSubst unionTCvSubst (TvSubst -> TCvSubst toTCv TvSubst s1) (TvSubst -> TCvSubst toTCv TvSubst s2) fromTCv :: TCvSubst -> TvSubst fromTCv :: TCvSubst -> TvSubst fromTCv (TCvSubst InScopeSet set TvSubstEnv tvsenv CvSubstEnv _) = InScopeSet -> TvSubstEnv -> TvSubst TvSubst InScopeSet set TvSubstEnv tvsenv promotedBoolTyCon :: TyCon promotedBoolTyCon :: TyCon promotedBoolTyCon = TyCon boolTyCon viewFunTy :: Type -> Maybe (Type, Type) viewFunTy :: Type -> Maybe (Type, Type) viewFunTy t :: Type t@(TyConApp TyCon _ [Type t1, Type t2]) | Type -> Bool Old.isFunTy Type t = (Type, Type) -> Maybe (Type, Type) forall a. a -> Maybe a Just (Type t1, Type t2) viewFunTy Type _ = Maybe (Type, Type) forall a. Maybe a Nothing #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 802 #else pattern FunTy :: Type -> Type -> Type pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where FunTy t1 t2 = Old.mkFunTy t1 t2 #endif tcUnifyTy :: Type -> Type -> Maybe TvSubst tcUnifyTy :: Type -> Type -> Maybe TvSubst tcUnifyTy Type t1 Type t2 = TCvSubst -> TvSubst fromTCv (TCvSubst -> TvSubst) -> Maybe TCvSubst -> Maybe TvSubst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Type -> Type -> Maybe TCvSubst Old.tcUnifyTy Type t1 Type t2 getEqTyCon :: TcPluginM TyCon getEqTyCon :: TcPluginM TyCon getEqTyCon = #if MIN_VERSION_ghc(8,8,1) TyCon -> TcPluginM TyCon forall (m :: * -> *) a. Monad m => a -> m a return TyCon TysWiredIn.eqTyCon #else tcLookupTyCon Old.eqTyConName #endif #else eqType :: Type -> Type -> Bool eqType = (==) getEqTyCon :: TcPluginM TyCon getEqTyCon = return Old.eqTyCon #endif getEqWitnessTyCon :: TcPluginM TyCon getEqWitnessTyCon :: TcPluginM TyCon getEqWitnessTyCon = do Module md <- ModuleName -> FastString -> TcPluginM Module lookupModule (String -> ModuleName mkModuleName String "Data.Type.Equality") (String -> FastString fsLit String "base") Name -> TcPluginM TyCon tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b =<< Module -> OccName -> TcPluginM Name lookupOrig Module md (String -> OccName mkTcOcc String ":~:") decompFunTy :: Type -> [Type] #if MIN_VERSION_ghc(8,10,1) decompFunTy :: Type -> [Type] decompFunTy (FunTy AnonArgFlag _ Type t1 Type t2) = Type t1 Type -> [Type] -> [Type] forall a. a -> [a] -> [a] : Type -> [Type] decompFunTy Type t2 #else decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2 #endif decompFunTy Type t = [Type t] newtype TypeEq = TypeEq { TypeEq -> Type runTypeEq :: Type } instance Eq TypeEq where == :: TypeEq -> TypeEq -> Bool (==) = Type -> Type -> Bool forall a. Data a => a -> a -> Bool geq (Type -> Type -> Bool) -> (TypeEq -> Type) -> TypeEq -> TypeEq -> Bool forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` TypeEq -> Type runTypeEq instance Ord TypeEq where compare :: TypeEq -> TypeEq -> Ordering compare = Type -> Type -> Ordering forall a. Data a => a -> a -> Ordering gcompare (Type -> Type -> Ordering) -> (TypeEq -> Type) -> TypeEq -> TypeEq -> Ordering forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` TypeEq -> Type runTypeEq isTrivial :: Old.PredType -> Bool isTrivial :: Type -> Bool isTrivial Type ty = case Type -> PredTree classifyPredType Type ty of EqPred EqRel _ Type l Type r -> Type l Type -> Type -> Bool `eqType` Type r PredTree _ -> Bool False normaliseGivens :: [Ct] -> TcPluginM [Ct] normaliseGivens :: [Ct] -> TcPluginM [Ct] normaliseGivens = #if MIN_VERSION_ghc(8,4,1) ([Ct] -> TcPluginM [Ct]) -> ([Ct] -> [Ct]) -> [Ct] -> TcPluginM [Ct] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Ct] -> TcPluginM [Ct] forall (m :: * -> *) a. Monad m => a -> m a return ([Ct] -> TcPluginM [Ct]) -> ([Ct] -> [Ct]) -> [Ct] -> TcPluginM [Ct] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Ct -> Bool) -> [Ct] -> [Ct] forall a. (a -> Bool) -> [a] -> [a] filter (Bool -> Bool not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Type -> Bool isTrivial (Type -> Bool) -> (Ct -> Type) -> Ct -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . CtEvidence -> Type ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type forall b c a. (b -> c) -> (a -> b) -> a -> c . Ct -> CtEvidence ctEvidence)) (([Ct] -> [Ct]) -> [Ct] -> TcPluginM [Ct]) -> ([Ct] -> [Ct] -> [Ct]) -> [Ct] -> [Ct] -> TcPluginM [Ct] forall b c a. (b -> c) -> (a -> b) -> a -> c . [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] (++) ([Ct] -> [Ct] -> TcPluginM [Ct]) -> ([Ct] -> [Ct]) -> [Ct] -> [Ct] -> TcPluginM [Ct] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Ct] -> [Ct] forall a. a -> a id ([Ct] -> [Ct] -> TcPluginM [Ct]) -> ([Ct] -> [Ct]) -> [Ct] -> TcPluginM [Ct] forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> [Ct] -> [Ct] Extra.flattenGivens #else mapM zonkCt #endif #if MIN_VERSION_ghc(8,4,1) type Substitution = [(TcTyVar, TcType)] #else type Substitution = TvSubst #endif subsCt :: Substitution -> Ct -> Ct subsCt :: Substitution -> Ct -> Ct subsCt = #if MIN_VERSION_ghc(8,4,1) Substitution -> Ct -> Ct Extra.substCt #else \subst ct -> ct { cc_ev = (cc_ev ct) {ctev_pred = substTy subst (ctev_pred (cc_ev ct))} } #endif subsType :: Substitution -> Type -> Type subsType :: Substitution -> Type -> Type subsType = #if MIN_VERSION_ghc(8,4,1) Substitution -> Type -> Type Extra.substType #else substTy #endif mkSubstitution :: [Ct] -> Substitution mkSubstitution :: [Ct] -> Substitution mkSubstitution = #if MIN_VERSION_ghc(8,4,1) (Substitution, [Ct]) -> Substitution forall a b. (a, b) -> a fst ((Substitution, [Ct]) -> Substitution) -> ([Ct] -> (Substitution, [Ct])) -> [Ct] -> Substitution forall b c a. (b -> c) -> (a -> b) -> a -> c . [((TcTyVar, Type), Ct)] -> (Substitution, [Ct]) forall a b. [(a, b)] -> ([a], [b]) unzip ([((TcTyVar, Type), Ct)] -> (Substitution, [Ct])) -> ([Ct] -> [((TcTyVar, Type), Ct)]) -> [Ct] -> (Substitution, [Ct]) forall b c a. (b -> c) -> (a -> b) -> a -> c . [Ct] -> [((TcTyVar, Type), Ct)] Extra.mkSubst' #else foldr (unionTvSubst . genSubst) emptyTvSubst #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804 genSubst :: Ct -> TvSubst genSubst ct = case classifyPredType (ctEvPred . ctEvidence $ ct) of EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u _ -> emptyTvSubst #endif classifyPredType :: Type -> PredTree classifyPredType :: Type -> PredTree classifyPredType Type ty = case Type -> PredTree Old.classifyPredType Type ty of e :: PredTree e@EqPred{} -> PredTree e ClassPred Class cls [Type _,Type t1,Type t2] | Class -> Name className Class cls Name -> Name -> Bool forall a. Eq a => a -> a -> Bool == Name eqTyConName -> EqRel -> Type -> Type -> PredTree EqPred EqRel NomEq Type t1 Type t2 PredTree e -> PredTree e