{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE ExplicitNamespaces    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiWayIf            #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE RoleAnnotations       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE ViewPatterns          #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module GHC.TypeLits.Normalise.Compat
  ( LookedUpTyCons(..), lookupTyCons
  , upToGivens
  , mkLEqNat
  , Relation, isNatRel

  , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList

  ) where

-- base
import Control.Arrow
  ( second )
import qualified Data.List.NonEmpty as NE
  ( toList )
import Data.Foldable
  ( asum )
import GHC.TypeNats
  ( CmpNat )
#if MIN_VERSION_ghc(9,3,0)
import qualified GHC.TypeError
  ( Assert )
#endif
#if MIN_VERSION_ghc(9,1,0)
import qualified Data.Type.Ord
  ( OrdCond, type (<=) )

#else
import GHC.TypeNats
  ( type (<=), type (<=?) )
#endif

-- ghc
import GHC.Builtin.Types
  ( isCTupleTyConName
  , promotedFalseDataCon, promotedTrueDataCon
  , promotedLTDataCon, promotedEQDataCon, promotedGTDataCon
  )
#if MIN_VERSION_ghc(9,1,0)
import GHC.Builtin.Types
  ( cTupleTyCon, cTupleDataCon )
#else
import GHC.Builtin.Types
  ( cTupleTyConName )
#endif
#if MIN_VERSION_ghc(9,7,0)
import GHC.Types.Unique.Map
  ( UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList )
#else
import GHC.Types.Unique
  ( Uniquable )
import GHC.Types.Unique.FM
  ( intersectUFM_C, nonDetEltsUFM )
#endif

-- ghc-tcplugin-api
import GHC.TcPlugin.API
import GHC.TcPlugin.API.TyConSubst
  ( TyConSubst, splitTyConApp_upTo )

--------------------------------------------------------------------------------

data LookedUpTyCons
  = LookedUpTyCons
    {
#if MIN_VERSION_ghc(9,3,0)
      LookedUpTyCons -> TyCon
assertTyCon :: TyCon,
#endif
#if MIN_VERSION_ghc(9,1,0)
       -- | @<= :: k -> k -> Constraint@
      LookedUpTyCons -> TyCon
ordCondTyCon :: TyCon,
      LookedUpTyCons -> TyCon
leqTyCon :: TyCon,
#else
       -- | @<= :: Nat -> Nat -> Constraint@
      leqNatTyCon :: TyCon,
      -- | @<=? :: Nat -> Nat -> Constraint@
      leqQNatTyCon :: TyCon,
#endif
      LookedUpTyCons -> TyCon
cmpNatTyCon :: TyCon,
      LookedUpTyCons -> TyCon
c0TyCon   :: TyCon,
      LookedUpTyCons -> DataCon
c0DataCon :: DataCon
    }

lookupTyCons :: TcPluginM Init LookedUpTyCons
lookupTyCons :: TcPluginM 'Init LookedUpTyCons
lookupTyCons = do
    TyCon
cmpNatT <- Name -> TcPluginM 'Init Name
forall (s :: TcPluginStage).
(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) =>
Name -> TcPluginM s Name
lookupTHName ''GHC.TypeNats.CmpNat TcPluginM 'Init Name
-> (Name -> TcPluginM 'Init TyCon) -> TcPluginM 'Init TyCon
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM 'Init TyCon
forall (m :: * -> *). MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon
#if MIN_VERSION_ghc(9,3,0)
    TyCon
assertT <- Name -> TcPluginM 'Init Name
forall (s :: TcPluginStage).
(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) =>
Name -> TcPluginM s Name
lookupTHName ''GHC.TypeError.Assert TcPluginM 'Init Name
-> (Name -> TcPluginM 'Init TyCon) -> TcPluginM 'Init TyCon
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM 'Init TyCon
forall (m :: * -> *). MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon
#endif
#if MIN_VERSION_ghc(9,1,0)
    TyCon
leqT    <- Name -> TcPluginM 'Init Name
forall (s :: TcPluginStage).
(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) =>
Name -> TcPluginM s Name
lookupTHName ''(Data.Type.Ord.<=) TcPluginM 'Init Name
-> (Name -> TcPluginM 'Init TyCon) -> TcPluginM 'Init TyCon
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM 'Init TyCon
forall (m :: * -> *). MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon
    TyCon
ordCond <- Name -> TcPluginM 'Init Name
forall (s :: TcPluginStage).
(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) =>
Name -> TcPluginM s Name
lookupTHName ''Data.Type.Ord.OrdCond TcPluginM 'Init Name
-> (Name -> TcPluginM 'Init TyCon) -> TcPluginM 'Init TyCon
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM 'Init TyCon
forall (m :: * -> *). MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon
    LookedUpTyCons -> TcPluginM 'Init LookedUpTyCons
forall a. a -> TcPluginM 'Init a
forall (m :: * -> *) a. Monad m => a -> m a
return (LookedUpTyCons -> TcPluginM 'Init LookedUpTyCons)
-> LookedUpTyCons -> TcPluginM 'Init LookedUpTyCons
forall a b. (a -> b) -> a -> b
$
      LookedUpTyCons
        { leqTyCon :: TyCon
leqTyCon     = TyCon
leqT
        , ordCondTyCon :: TyCon
ordCondTyCon = TyCon
ordCond
#  if MIN_VERSION_ghc(9,3,0)
        , assertTyCon :: TyCon
assertTyCon  = TyCon
assertT
#  endif
        , cmpNatTyCon :: TyCon
cmpNatTyCon  = TyCon
cmpNatT
        , c0TyCon :: TyCon
c0TyCon      = Arity -> TyCon
cTupleTyCon Arity
0
        , c0DataCon :: DataCon
c0DataCon    = Arity -> DataCon
cTupleDataCon Arity
0
        }
#else
    leqT  <- lookupTHName ''(GHC.TypeNats.<=)  >>= tcLookupTyCon
    leqQT <- lookupTHName ''(GHC.TypeNats.<=?) >>= tcLookupTyCon
    c0T   <- tcLookupTyCon (cTupleTyConName 0)
    let c0D = tyConSingleDataCon c0T
      -- somehow looking up the 0-tuple data constructor fails
      -- with interface file errors, so use tyConSingleDataCon
    return $
      LookedUpTyCons
        { leqNatTyCon  = leqT
        , leqQNatTyCon = leqQT
        , c0TyCon      = c0T
        , c0DataCon    = c0D
        , cmpNatTyCon  = cmpNatT
        }
#endif

-- | The constraint @(a <= b)@.
mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType
mkLEqNat :: LookedUpTyCons -> Type -> Type -> Type
mkLEqNat LookedUpTyCons
tcs Type
a Type
b =
#if MIN_VERSION_ghc(9,3,0)
  -- Starting from GHC 9.3, (a <= b) turns into 'Assert (a <=? b) msg'.
  -- We prefer to emit 'Assert (a <=? b) msg ~ (() :: Constraint)',
  -- in order to avoid creating an Irred constraint.
  Role -> Type -> Type -> Type
mkEqPredRole Role
Nominal
    (TyCon -> [Type] -> Type
mkTyConApp (LookedUpTyCons -> TyCon
leqTyCon LookedUpTyCons
tcs) [Type
natKind, Type
a, Type
b])
    (TyCon -> Type
mkTyConTy (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ LookedUpTyCons -> TyCon
c0TyCon LookedUpTyCons
tcs)
#elif MIN_VERSION_ghc(9,1,0)
  mkTyConApp (leqTyCon tcs) [natKind, a, b]
#else
  mkTyConApp (leqNatTyCon tcs) [a, b]
#endif

-- | Is this type 'True' or 'False'?
boolean_maybe :: TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe :: TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst =
  TyConSubst
-> (TyCon -> [Type] -> Maybe (Bool, [Coercion]))
-> Type
-> Maybe (Bool, [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst ( \ TyCon
tc [Type]
tys -> (, []) (Bool -> (Bool, [Coercion]))
-> Maybe Bool -> Maybe (Bool, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> Maybe Bool
forall {a}. TyCon -> [a] -> Maybe Bool
go TyCon
tc [Type]
tys )
  where
    go :: TyCon -> [a] -> Maybe Bool
go TyCon
tc []
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
      = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
      = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    go TyCon
_ [a]
_ = Maybe Bool
forall a. Maybe a
Nothing

-- | Is this type 'LT', 'EQ' or 'GT'?
ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion])
ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion])
ordering_maybe TyConSubst
givensTyConSubst =
  TyConSubst
-> (TyCon -> [Type] -> Maybe (Ordering, [Coercion]))
-> Type
-> Maybe (Ordering, [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst ( \ TyCon
tc [Type]
tys -> (, []) (Ordering -> (Ordering, [Coercion]))
-> Maybe Ordering -> Maybe (Ordering, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> Maybe Ordering
forall {a}. TyCon -> [a] -> Maybe Ordering
go TyCon
tc [Type]
tys )
  where
    go :: TyCon -> [a] -> Maybe Ordering
go TyCon
tc []
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedLTDataCon
      = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedEQDataCon
      = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedGTDataCon
      = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
    go TyCon
_ [a]
_ = Maybe Ordering
forall a. Maybe a
Nothing

#if MIN_VERSION_ghc(9,1,0)
cmpNat_maybe :: LookedUpTyCons -> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])
cmpNat_maybe :: LookedUpTyCons
-> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])
cmpNat_maybe LookedUpTyCons
tcs TyConSubst
givensTyConSubst =
  TyConSubst
-> (TyCon -> [Type] -> Maybe ((Type, Type), [Coercion]))
-> Type
-> Maybe ((Type, Type), [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst ( \ TyCon
tc [Type]
tys -> (, []) ((Type, Type) -> ((Type, Type), [Coercion]))
-> Maybe (Type, Type) -> Maybe ((Type, Type), [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> Maybe (Type, Type)
forall {b}. TyCon -> [b] -> Maybe (b, b)
go TyCon
tc [Type]
tys )
  where
    go :: TyCon -> [b] -> Maybe (b, b)
go TyCon
tc [b
x,b
y]
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== LookedUpTyCons -> TyCon
cmpNatTyCon LookedUpTyCons
tcs
      = (b, b) -> Maybe (b, b)
forall a. a -> Maybe a
Just (b
x,b
y)
    go TyCon
_ [b]
_ = Maybe (b, b)
forall a. Maybe a
Nothing
#endif

-- | Is this type @() :: Constraint@?
unitCTuple_maybe :: TyConSubst -> PredType -> Maybe ((), [Coercion])
unitCTuple_maybe :: TyConSubst -> Type -> Maybe ((), [Coercion])
unitCTuple_maybe TyConSubst
givensTyConSubst =
  TyConSubst
-> (TyCon -> [Type] -> Maybe ((), [Coercion]))
-> Type
-> Maybe ((), [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst ( \ TyCon
tc [Type]
tys -> (, []) (() -> ((), [Coercion])) -> Maybe () -> Maybe ((), [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> Maybe ()
forall {a}. TyCon -> [a] -> Maybe ()
go TyCon
tc [Type]
tys )
    where
      go :: TyCon -> [a] -> Maybe ()
go TyCon
tc []
        | Name -> Bool
isCTupleTyConName (TyCon -> Name
tyConName TyCon
tc)
        = () -> Maybe ()
forall a. a -> Maybe a
Just ()
      go TyCon
_ [a]
_ = Maybe ()
forall a. Maybe a
Nothing

-- | A relation between two natural numbers, @((x,y), mbRel)@.
--
-- The @mbRel@ value indicates the kind of relation:
--
--  - @Nothing@ <=> @x ~ y@,
--  - @Just b@ <=> @(x <=? y) ~ b@.
type Relation = ((Type, Type), Maybe Bool)

{- Note [Recognising Nat inequalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Recognising whether a type is an inequality between two natural numbers is
not as straightforward as one might initially think. The problem is that there
are many different built-in types that can be used to represent an equality of
natural numbers:

  1. GHC.TypeNats.CmpNat, returning Ordering.
     This type family is primitive (on all GHC versions).
  2. GHC.TypeNats.<=?, returning a Boolean.
     This type family is primitive prior to GHC 9.1, but is defined in
     terms of the 'OrdCond' type family starting in GHC 9.1.

     (NB: it also becomes poly-kinded starting in GHC 9.1.)
  3. GHC.TypeNats.<=, which is defined:
    (a) as @x <= y@ <=> @(x <=? y) ~ True@ in GHC prior to 9.3.
    (b) as @Assert (x <=? y) ...@ in GHC 9.3 and above.

To catch all of these, we must thus handle all of the following type families:

  Case 1. CmpNat.
  Case 2. (<=?) in GHC 9.1 and prior.
  Case 3. OrdCond in GHC 9.1 and later.
  Case 4. Assert, in GHC 9.3 and later.

These are all the built-in type families defined in GHC used to express
inequalities between natural numbers.
-}

-- | Is this an equality or inequality between two natural numbers?
--
-- See Note [Recognising Nat inequalities].
isNatRel :: LookedUpTyCons -> TyConSubst -> PredType -> Maybe (Relation, [Coercion])
isNatRel :: LookedUpTyCons
-> TyConSubst -> Type -> Maybe (Relation, [Coercion])
isNatRel LookedUpTyCons
tcs TyConSubst
givensTyConSubst Type
ty0
  | EqPred EqRel
NomEq Type
x Type
y <- Type -> Pred
classifyPredType Type
ty0
  = if
      -- (b :: Bool) ~ y
      | Just ( Bool
b, [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst Type
x
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> Maybe (Relation, [Coercion])
booleanRel Bool
b Type
y
      -- x ~ (b :: Bool)
      | Just ( Bool
b, [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst Type
y
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> Maybe (Relation, [Coercion])
booleanRel Bool
b Type
x
      | Just ( Ordering
o, [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe (Ordering, [Coercion])
ordering_maybe TyConSubst
givensTyConSubst Type
x
      -- (o :: Ordering) ~ y
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ordering -> Type -> Maybe (Relation, [Coercion])
orderingRel Ordering
o Type
y
      | Just ( Ordering
o, [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe (Ordering, [Coercion])
ordering_maybe TyConSubst
givensTyConSubst Type
y
      -- x ~ (o :: Ordering)
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ordering -> Type -> Maybe (Relation, [Coercion])
orderingRel Ordering
o Type
x
      -- (() :: Constraint) ~ y
      | Just ( (), [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe ((), [Coercion])
unitCTuple_maybe TyConSubst
givensTyConSubst Type
x
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe (Relation, [Coercion])
goTy Type
y
      -- x ~ (() :: Constraint)
      | Just ( (), [Coercion]
cos1 ) <- TyConSubst -> Type -> Maybe ((), [Coercion])
unitCTuple_maybe TyConSubst
givensTyConSubst Type
y
      -> ([Coercion] -> [Coercion])
-> (Relation, [Coercion]) -> (Relation, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos1 ) ((Relation, [Coercion]) -> (Relation, [Coercion]))
-> Maybe (Relation, [Coercion]) -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe (Relation, [Coercion])
goTy Type
x
      | Bool
otherwise
      -> Maybe (Relation, [Coercion])
forall a. Maybe a
Nothing
  | Bool
otherwise
  = Type -> Maybe (Relation, [Coercion])
goTy Type
ty0
  where
    goTy :: PredType -> Maybe (Relation, [Coercion])
    goTy :: Type -> Maybe (Relation, [Coercion])
goTy = TyConSubst
-> (TyCon -> [Type] -> Maybe (Relation, [Coercion]))
-> Type
-> Maybe (Relation, [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst TyCon -> [Type] -> Maybe (Relation, [Coercion])
goTc

    goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion])
    goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion])
goTc TyCon
_tc [Type]
_tys
#if MIN_VERSION_ghc(9,3,0)
      -- Look through 'Assert'.
      -- Case 4 in Note [Recognising Nat inequalities]
      | TyCon
_tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== LookedUpTyCons -> TyCon
assertTyCon LookedUpTyCons
tcs
      , [Type
ty, Type
_] <- [Type]
_tys
      = Bool -> Type -> Maybe (Relation, [Coercion])
booleanRel Bool
True Type
ty
#endif
      | Bool
otherwise
      = Maybe (Relation, [Coercion])
forall a. Maybe a
Nothing

    -- Recognise whether @(b :: Bool) ~ ty@ is an equality/inequality
    booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion])
    booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion])
booleanRel Bool
b = TyConSubst
-> (TyCon -> [Type] -> Maybe (Relation, [Coercion]))
-> Type
-> Maybe (Relation, [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst (Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
goBoolean Bool
b)

    goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
    goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
goBoolean Bool
b TyCon
tc [Type]
tys
#if MIN_VERSION_ghc(9,1,0)
      -- OrdCond (CmpNat x y) lt eq gt ~ b
      -- Case 3 in Note [Recognising Nat inequalities]
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== LookedUpTyCons -> TyCon
ordCondTyCon LookedUpTyCons
tcs
      , [Type
_,Type
cmp,Type
ltTy,Type
eqTy,Type
gtTy] <- [Type]
tys
      , Just (Bool
lt, [Coercion]
cos1) <- TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst Type
ltTy
      , Just (Bool
eq, [Coercion]
cos2) <- TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst Type
eqTy
      , Just (Bool
gt, [Coercion]
cos3) <- TyConSubst -> Type -> Maybe (Bool, [Coercion])
boolean_maybe TyConSubst
givensTyConSubst Type
gtTy
      , Just ((Type
x,Type
y), [Coercion]
cos4) <- LookedUpTyCons
-> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])
cmpNat_maybe LookedUpTyCons
tcs TyConSubst
givensTyConSubst Type
cmp
      = ( , [Coercion]
cos1 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos2 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos3 [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
cos4 ) (Relation -> (Relation, [Coercion]))
-> Maybe Relation -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        if -- (x <= y) ~ b
          | Bool
lt Bool -> Bool -> Bool
&& Bool
eq Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
gt
          -> Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
x,Type
y), Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b)
          -- (x < y) ~ b
          --   <=>
          -- (y <= x) ~ not b
          | Bool
lt Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
eq Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
gt
          -> Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
y,Type
x), Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b)
          -- (x >= y) ~ b
          --  <=>
          -- (y <= x) ~ b
          | Bool -> Bool
not Bool
lt Bool -> Bool -> Bool
&& Bool
eq Bool -> Bool -> Bool
&& Bool
gt
          -> Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
y,Type
x), Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b)
          -- (x > y) ~ b
          --   <=>
          -- (x <= y) ~ not b
          | Bool -> Bool
not Bool
lt Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
eq Bool -> Bool -> Bool
&& Bool
gt
          -> Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
x,Type
y), Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b)
          -- x ~ y
          |  ( Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
lt Bool -> Bool -> Bool
&& Bool
eq Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
gt )
          Bool -> Bool -> Bool
|| ( Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& Bool
lt Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
eq Bool -> Bool -> Bool
&& Bool
gt )
          -> Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
x,Type
y), Maybe Bool
forall a. Maybe a
Nothing)
          | Bool
otherwise
          -> Maybe Relation
forall a. Maybe a
Nothing
#else
      -- (x <=? y) ~ b
      -- Case 2 in Note [Recognising Nat inequalities]
      | tc == leqQNatTyCon tcs
      , [x,y] <- tys
      = Just (((x,y), Just b), [])
#endif
      | Bool
otherwise
      = Maybe (Relation, [Coercion])
forall a. Maybe a
Nothing

    -- Recognise whether @(o :: Ordering) ~ ty@ is an equality/inequality
    orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion])
    orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion])
orderingRel Ordering
o = TyConSubst
-> (TyCon -> [Type] -> Maybe (Relation, [Coercion]))
-> Type
-> Maybe (Relation, [Coercion])
forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst (Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
goOrdering Ordering
o)

    goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
    goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])
goOrdering Ordering
o TyCon
tc [Type]
tys
      -- CmpNat x y ~ o
      -- Case 1 in Note [Recognising Nat inequalities]
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== LookedUpTyCons -> TyCon
cmpNatTyCon LookedUpTyCons
tcs
      , [Type
x,Type
y] <- [Type]
tys
      = ( , [] ) (Relation -> (Relation, [Coercion]))
-> Maybe Relation -> Maybe (Relation, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        case Ordering
o of
          Ordering
EQ ->
            -- x ~ y
            Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
x,Type
y), Maybe Bool
forall a. Maybe a
Nothing)
          Ordering
LT ->
            -- x < y  <=>  (y <= x) ~ False
            Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
y,Type
x), Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
          Ordering
GT ->
            -- x > y  <=>  (x <= y) ~ False
            Relation -> Maybe Relation
forall a. a -> Maybe a
Just ((Type
x,Type
y), Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
      | Bool
otherwise
      = Maybe (Relation, [Coercion])
forall a. Maybe a
Nothing

upToGivens :: TyConSubst -> (TyCon -> [Type] -> Maybe (a, [Coercion])) -> Type -> Maybe (a, [Coercion])
upToGivens :: forall a.
TyConSubst
-> (TyCon -> [Type] -> Maybe (a, [Coercion]))
-> Type
-> Maybe (a, [Coercion])
upToGivens TyConSubst
givensTyConSubst TyCon -> [Type] -> Maybe (a, [Coercion])
f Type
ty =
  [Maybe (a, [Coercion])] -> Maybe (a, [Coercion])
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([Maybe (a, [Coercion])] -> Maybe (a, [Coercion]))
-> [Maybe (a, [Coercion])] -> Maybe (a, [Coercion])
forall a b. (a -> b) -> a -> b
$ ((TyCon, [Type], [Coercion]) -> Maybe (a, [Coercion]))
-> [(TyCon, [Type], [Coercion])] -> [Maybe (a, [Coercion])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (TyCon
tc, [Type]
tys, [Coercion]
deps) -> ([Coercion] -> [Coercion]) -> (a, [Coercion]) -> (a, [Coercion])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ( [Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ ) ((a, [Coercion]) -> (a, [Coercion]))
-> Maybe (a, [Coercion]) -> Maybe (a, [Coercion])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> Maybe (a, [Coercion])
f TyCon
tc [Type]
tys ) ([(TyCon, [Type], [Coercion])] -> [Maybe (a, [Coercion])])
-> [(TyCon, [Type], [Coercion])] -> [Maybe (a, [Coercion])]
forall a b. (a -> b) -> a -> b
$
    [(TyCon, [Type], [Coercion])]
-> (NonEmpty (TyCon, [Type], [Coercion])
    -> [(TyCon, [Type], [Coercion])])
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
-> [(TyCon, [Type], [Coercion])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] NonEmpty (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
forall a. NonEmpty a -> [a]
NE.toList (Maybe (NonEmpty (TyCon, [Type], [Coercion]))
 -> [(TyCon, [Type], [Coercion])])
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
-> [(TyCon, [Type], [Coercion])]
forall a b. (a -> b) -> a -> b
$ TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo TyConSubst
givensTyConSubst Type
ty

--------------------------------------------------------------------------------
#if !MIN_VERSION_ghc(9,7,0)

newtype UniqMap k a = UniqMap ( UniqFM k (k, a) )
    deriving (Eq, Functor)
type role UniqMap nominal representational

intersectUniqMap_C :: (a -> b -> c) -> UniqMap k a -> UniqMap k b -> UniqMap k c
intersectUniqMap_C f (UniqMap m1) (UniqMap m2) = UniqMap $ intersectUFM_C (\(k, a) (_, b) -> (k, f a b)) m1 m2
{-# INLINE intersectUniqMap_C #-}

listToUniqMap :: Uniquable k => [(k,a)] -> UniqMap k a
listToUniqMap kvs = UniqMap (listToUFM [ (k,(k,v)) | (k,v) <- kvs])
{-# INLINE listToUniqMap #-}

nonDetUniqMapToList :: UniqMap k a -> [(k, a)]
nonDetUniqMapToList (UniqMap m) = nonDetEltsUFM m
{-# INLINE nonDetUniqMapToList #-}

#endif