{-# 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