{-|
Copyright  :  (C) 2015-2016, University of Twente,
                  2017     , QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

A type checker plugin for GHC that can solve /equalities/ of types of kind
'GHC.TypeLits.Nat', where these types are either:

* Type-level naturals
* Type variables
* Applications of the arithmetic expressions @(+,-,*,^)@.

It solves these equalities by normalising them to /sort-of/
'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a
simple syntactic equality.

For example, this solver can prove the equality between:

@
(x + 2)^(y + 2)
@

and

@
4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
@

Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form
of the former.

To use the plugin, add

@
{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
@

To the header of your file.

== Treating subtraction as addition with a negated number

If you are absolutely sure that your subtractions can /never/ lead to (a locally)
negative number, you can ask the plugin to treat subtraction as addition with
a negated operand by additionally adding:

@
{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
@

to the header of your file, thereby allowing to use associativity and
commutativity rules when proving constraints involving subtractions. Note that
this option can lead to unsound behaviour and should be handled with extreme
care.

=== When it leads to unsound behaviour

For example, enabling the /allow-negated-numbers/ feature would allow
you to prove:

@
(n - 1) + 1 ~ n
@

/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the
subtraction @n-1@ would be locally negative and hence not be a natural number.

This would allow the following erroneous definition:

@
data Fin (n :: Nat) where
  FZ :: Fin (n + 1)
  FS :: Fin n -> Fin (n + 1)

f :: forall n . Natural -> Fin n
f n = case of
  0 -> FZ
  x -> FS (f \@(n-1) (x - 1))

fs :: [Fin 0]
fs = f \<$\> [0..]
@

=== When it might be Okay

This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>
library.

When you have:

@
-- | Singleton type for the number of repetitions of an element.
data Times (n :: Nat) where
    T :: Times n

-- | An element of a "run-length encoded" vector, containing the value and
-- the number of repetitions
data Elem :: Type -> Nat -> Type where
    (:*) :: t -> Times n -> Elem t n

-- | A length-indexed vector, optimised for repetitions.
data OptVector :: Type -> Nat -> Type where
    End  :: OptVector t 0
    (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n
@

And you want to define:

@
-- | Append two optimised vectors.
type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
    ys        ++ End = ys
    End       ++ ys = ys
    (x :- xs) ++ ys = x :- (xs ++ ys)
@

then the last line will give rise to the constraint:

@
(n-l)+m ~ (n+m)-l
@

because:

@
x  :: Elem t l
xs :: OptVector t (n-l)
ys :: OptVector t m
@

In this case it's okay to add

@
{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
@

if you can convince yourself you will never be able to construct a:

@
xs :: OptVector t (n-l)
@

where /n-l/ is a negative number.
-}

{-# LANGUAGE CPP             #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE ViewPatterns    #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE NamedFieldPuns  #-}
{-# LANGUAGE TupleSections   #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module GHC.TypeLits.Normalise
  ( plugin )
where

-- external
import Control.Arrow       (second)
import Control.Monad       ((<=<))
#if !MIN_VERSION_ghc(8,4,1)
import Control.Monad       (replicateM)
#endif
import Control.Monad.Trans.Writer.Strict
import Data.Either         (rights)
import Data.List           (intersect, stripPrefix)
import Data.Maybe          (mapMaybe)
import Data.Set            (Set, empty, toList)
import GHC.TcPluginM.Extra (tracePlugin)
import qualified GHC.TcPluginM.Extra as TcPluginM
#if MIN_VERSION_ghc(8,4,0)
import GHC.TcPluginM.Extra (flattenGivens)
#endif
import Text.Read           (readMaybe)

-- GHC API
#if MIN_VERSION_ghc(8,5,0)
import CoreSyn    (Expr (..))
#endif
import Outputable (Outputable (..), (<+>), ($$), text)
import Plugins    (Plugin (..), defaultPlugin)
#if MIN_VERSION_ghc(8,6,0)
import Plugins    (purePlugin)
#endif
import PrelNames  (knownNatClassName)
import TcEvidence (EvTerm (..))
#if !MIN_VERSION_ghc(8,4,0)
import TcPluginM  (zonkCt)
#endif
import TcPluginM  (TcPluginM, tcPluginTrace)
import TcRnTypes  (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,
                   isWanted, mkNonCanonical)
import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType,
                   classifyPredType, eqType, getEqPredTys, mkTyVarTy)
import TysWiredIn (typeNatKind)

import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
                   mkNomReflCo, mkUnivCo)
import TcPluginM  (newCoercionHole, newFlexiTyVar, tcLookupClass)
import TcRnTypes
  (CtEvidence (..), CtLoc, TcEvDest (..), ctEvLoc, ctLoc, ctLocSpan, isGiven,
   setCtLoc, setCtLocSpan)
#if MIN_VERSION_ghc(8,2,0)
import TcRnTypes  (ShadowInfo (WDeriv))
#endif
import TyCoRep    (UnivCoProvenance (..))
import Type       (mkClassPred, mkPrimEqPred)
import TcType     (typeKind)
import TyCoRep    (Type (..))
import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                   typeNatSubTyCon)

import TcTypeNats (typeNatLeqTyCon)
import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)

-- internal
import GHC.TypeLits.Normalise.Unify

-- | To use the plugin, add
--
-- @
-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
-- @
--
-- To the header of your file.
plugin :: Plugin
plugin :: Plugin
plugin
  = Plugin
defaultPlugin
  { tcPlugin :: TcPlugin
tcPlugin = ([Opts -> Opts] -> TcPlugin)
-> Maybe [Opts -> Opts] -> Maybe TcPlugin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Opts -> TcPlugin
normalisePlugin (Opts -> TcPlugin)
-> ([Opts -> Opts] -> Opts) -> [Opts -> Opts] -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Opts -> Opts) -> Opts -> Opts) -> Opts -> [Opts -> Opts] -> Opts
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Opts -> Opts) -> Opts -> Opts
forall a. a -> a
id Opts
defaultOpts) (Maybe [Opts -> Opts] -> Maybe TcPlugin)
-> ([[Char]] -> Maybe [Opts -> Opts]) -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Maybe (Opts -> Opts))
-> [[Char]] -> Maybe [Opts -> Opts]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [Char] -> Maybe (Opts -> Opts)
parseArgument
#if MIN_VERSION_ghc(8,6,0)
  , pluginRecompile :: [[Char]] -> IO PluginRecompile
pluginRecompile = [[Char]] -> IO PluginRecompile
purePlugin
#endif
  }
 where
  parseArgument :: [Char] -> Maybe (Opts -> Opts)
parseArgument "allow-negated-numbers" = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ opts :: Opts
opts -> Opts
opts { negNumbers :: Bool
negNumbers = Bool
True })
  parseArgument ([Char] -> Maybe Word
forall a. Read a => [Char] -> Maybe a
readMaybe ([Char] -> Maybe Word)
-> ([Char] -> Maybe [Char]) -> [Char] -> Maybe Word
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [Char] -> [Char] -> Maybe [Char]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "depth=" -> Just depth :: Word
depth) = (Opts -> Opts) -> Maybe (Opts -> Opts)
forall a. a -> Maybe a
Just (\ opts :: Opts
opts -> Opts
opts { Word
depth :: Word
depth :: Word
depth })
  parseArgument _ = Maybe (Opts -> Opts)
forall a. Maybe a
Nothing
  defaultOpts :: Opts
defaultOpts = Opts :: Bool -> Word -> Opts
Opts { negNumbers :: Bool
negNumbers = Bool
False, depth :: Word
depth = 5 }

data Opts = Opts { Opts -> Bool
negNumbers :: Bool, Opts -> Word
depth :: Word }

normalisePlugin :: Opts -> TcPlugin
normalisePlugin :: Opts -> TcPlugin
normalisePlugin opts :: Opts
opts = [Char] -> TcPlugin -> TcPlugin
tracePlugin "ghc-typelits-natnormalise"
  TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin { tcPluginInit :: TcPluginM ()
tcPluginInit  = () -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           , tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = TcPluginSolver -> () -> TcPluginSolver
forall a b. a -> b -> a
const (Opts -> TcPluginSolver
decideEqualSOP Opts
opts)
           , tcPluginStop :: () -> TcPluginM ()
tcPluginStop  = TcPluginM () -> () -> TcPluginM ()
forall a b. a -> b -> a
const (() -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }

decideEqualSOP
  :: Opts
  -> [Ct]
  -> [Ct]
  -> [Ct]
  -> TcPluginM TcPluginResult
decideEqualSOP :: Opts -> TcPluginSolver
decideEqualSOP _opts :: Opts
_opts _givens :: [Ct]
_givens _deriveds :: [Ct]
_deriveds []      = TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [])
decideEqualSOP opts :: Opts
opts  givens :: [Ct]
givens  _deriveds :: [Ct]
_deriveds wanteds :: [Ct]
wanteds = do
    -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
    let wanteds' :: [Ct]
wanteds' = (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool) -> (Ct -> CtEvidence) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
wanteds
    let unit_wanteds :: [(Either NatEquality NatInEquality, [(Type, Type)])]
unit_wanteds = (Ct -> Maybe (Either NatEquality NatInEquality, [(Type, Type)]))
-> [Ct] -> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
toNatEquality [Ct]
wanteds'
    case [(Either NatEquality NatInEquality, [(Type, Type)])]
unit_wanteds of
      [] -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [])
      _  -> do
#if MIN_VERSION_ghc(8,4,0)
        let unit_givens :: [(Either NatEquality NatInEquality, [(Type, Type)])]
unit_givens = (Ct -> Maybe (Either NatEquality NatInEquality, [(Type, Type)]))
-> [Ct] -> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ct -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
toNatEquality ([Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct] -> [Ct]
flattenGivens [Ct]
givens)
#else
        unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens
#endif
        SimplifyResult
sr <- Opts
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simplifyNats Opts
opts [(Either NatEquality NatInEquality, [(Type, Type)])]
unit_givens [(Either NatEquality NatInEquality, [(Type, Type)])]
unit_wanteds
        [Char] -> SDoc -> TcPluginM ()
tcPluginTrace "normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
        case SimplifyResult
sr of
          Simplified evs :: [((EvTerm, Ct), [Ct])]
evs -> do
            let solved :: [((EvTerm, Ct), [Ct])]
solved = (((EvTerm, Ct), [Ct]) -> Bool)
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool)
-> (((EvTerm, Ct), [Ct]) -> CtEvidence)
-> ((EvTerm, Ct), [Ct])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence (Ct -> CtEvidence)
-> (((EvTerm, Ct), [Ct]) -> Ct)
-> ((EvTerm, Ct), [Ct])
-> CtEvidence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((_,x :: Ct
x),_) -> Ct
x)) [((EvTerm, Ct), [Ct])]
evs
                (solved' :: [(EvTerm, Ct)]
solved',newWanteds :: [Ct]
newWanteds) = ([[Ct]] -> [Ct])
-> ([(EvTerm, Ct)], [[Ct]]) -> ([(EvTerm, Ct)], [Ct])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip [((EvTerm, Ct), [Ct])]
solved)
            TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [(EvTerm, Ct)]
solved' [Ct]
newWanteds)
          Impossible eq :: Either NatEquality NatInEquality
eq -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginResult
TcPluginContradiction [Either NatEquality NatInEquality -> Ct
fromNatEquality Either NatEquality NatInEquality
eq])

type NatEquality   = (Ct,CoreSOP,CoreSOP)
type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))

fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality (Left  (ct :: Ct
ct, _, _)) = Ct
ct
fromNatEquality (Right (ct :: Ct
ct, _))    = Ct
ct

data SimplifyResult
  = Simplified [((EvTerm,Ct),[Ct])]
  | Impossible (Either NatEquality NatInEquality)

instance Outputable SimplifyResult where
  ppr :: SimplifyResult -> SDoc
ppr (Simplified evs :: [((EvTerm, Ct), [Ct])]
evs) = [Char] -> SDoc
text "Simplified" SDoc -> SDoc -> SDoc
$$ [((EvTerm, Ct), [Ct])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [((EvTerm, Ct), [Ct])]
evs
  ppr (Impossible eq :: Either NatEquality NatInEquality
eq)  = [Char] -> SDoc
text "Impossible" SDoc -> SDoc -> SDoc
<+> Either NatEquality NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either NatEquality NatInEquality
eq

simplifyNats
  :: Opts
  -- ^ Allow negated numbers (potentially unsound!)
  -> [(Either NatEquality NatInEquality,[(Type,Type)])]
  -- ^ Given constraints
  -> [(Either NatEquality NatInEquality,[(Type,Type)])]
  -- ^ Wanted constraints
  -> TcPluginM SimplifyResult
simplifyNats :: Opts
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simplifyNats (Opts {..}) eqsG :: [(Either NatEquality NatInEquality, [(Type, Type)])]
eqsG eqsW :: [(Either NatEquality NatInEquality, [(Type, Type)])]
eqsW =
    let eqs :: [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs = ((Either NatEquality NatInEquality, [(Type, Type)])
 -> (Either NatEquality NatInEquality, [(Type, Type)]))
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Type, Type)] -> [(Type, Type)])
-> (Either NatEquality NatInEquality, [(Type, Type)])
-> (Either NatEquality NatInEquality, [(Type, Type)])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a b. a -> b -> a
const [])) [(Either NatEquality NatInEquality, [(Type, Type)])]
eqsG [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(Type, Type)])]
eqsW
    in  [Char] -> SDoc -> TcPluginM ()
tcPluginTrace "simplifyNats" ([(Either NatEquality NatInEquality, [(Type, Type)])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs) TcPluginM ()
-> TcPluginM SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [] [] [] [] [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs
  where
    -- If we allow negated numbers we simply do not emit the inequalities
    -- derived from the subtractions that are converted to additions with a
    -- negated operand
    subToPred :: [(Type, Type)] -> [(Type, Type)]
subToPred | Bool
negNumbers = [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a b. a -> b -> a
const []
              | Bool
otherwise  = ((Type, Type) -> (Type, Type)) -> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> (Type, Type)
subtractionToPred

    simples :: [CoreUnify]
            -> [((EvTerm, Ct), [Ct])]
            -> [(CoreSOP,CoreSOP,Bool)]
            -> [(Either NatEquality NatInEquality,[(Type,Type)])]
            -> [(Either NatEquality NatInEquality,[(Type,Type)])]
            -> TcPluginM SimplifyResult
    simples :: [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples _subst :: [CoreUnify]
_subst evs :: [((EvTerm, Ct), [Ct])]
evs _leqsG :: [(CoreSOP, CoreSOP, Bool)]
_leqsG _xs :: [(Either NatEquality NatInEquality, [(Type, Type)])]
_xs [] = SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([((EvTerm, Ct), [Ct])] -> SimplifyResult
Simplified [((EvTerm, Ct), [Ct])]
evs)
    simples subst :: [CoreUnify]
subst evs :: [((EvTerm, Ct), [Ct])]
evs leqsG :: [(CoreSOP, CoreSOP, Bool)]
leqsG xs :: [(Either NatEquality NatInEquality, [(Type, Type)])]
xs (eq :: (Either NatEquality NatInEquality, [(Type, Type)])
eq@(Left (ct :: Ct
ct,u :: CoreSOP
u,v :: CoreSOP
v),k :: [(Type, Type)]
k):eqs' :: [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs') = do
      let u' :: CoreSOP
u' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
u
          v' :: CoreSOP
v' = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
v
      UnifyResult
ur <- Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats Ct
ct CoreSOP
u' CoreSOP
v'
      [Char] -> SDoc -> TcPluginM ()
tcPluginTrace "unifyNats result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
ur of
        Win -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ([(Type, Type)] -> [(Type, Type)]
subToPred [(Type, Type)]
k)
          [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG [] ([(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs')
        Lose -> if [((EvTerm, Ct), [Ct])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((EvTerm, Ct), [Ct])]
evs Bool -> Bool -> Bool
&& [(Either NatEquality NatInEquality, [(Type, Type)])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'
                   then SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NatEquality NatInEquality -> SimplifyResult
Impossible ((Either NatEquality NatInEquality, [(Type, Type)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst (Either NatEquality NatInEquality, [(Type, Type)])
eq))
                   else [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG [(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'
        Draw [] -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [] ((Either NatEquality NatInEquality, [(Type, Type)])
eq(Either NatEquality NatInEquality, [(Type, Type)])
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either NatEquality NatInEquality, [(Type, Type)])]
xs) [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'
        Draw subst' :: [CoreUnify]
subst' -> do
          Maybe ((EvTerm, Ct), [Ct])
evM <- Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ((CoreUnify -> (Type, Type)) -> [CoreUnify] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map CoreUnify -> (Type, Type)
unifyItemToPredType [CoreUnify]
subst' [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++
                                   [(Type, Type)] -> [(Type, Type)]
subToPred [(Type, Type)]
k)
          let leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = CoreSOP -> CoreSOP -> [(CoreSOP, CoreSOP, Bool)]
forall a. a -> a -> [(a, a, Bool)]
eqToLeq CoreSOP
u' CoreSOP
v' [(CoreSOP, CoreSOP, Bool)]
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. [a] -> [a] -> [a]
++ [(CoreSOP, CoreSOP, Bool)]
leqsG
                     | Bool
otherwise  = [(CoreSOP, CoreSOP, Bool)]
leqsG
          case Maybe ((EvTerm, Ct), [Ct])
evM of
            Nothing -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'
            Just ev :: ((EvTerm, Ct), [Ct])
ev ->
              [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples ([CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall v c.
(Ord v, Ord c) =>
[UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [CoreUnify]
subst' [CoreUnify]
subst [CoreUnify] -> [CoreUnify] -> [CoreUnify]
forall a. [a] -> [a] -> [a]
++ [CoreUnify]
subst')
                      (((EvTerm, Ct), [Ct])
ev((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) [(CoreSOP, CoreSOP, Bool)]
leqsG' [] ([(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a. [a] -> [a] -> [a]
++ [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs')
    simples subst :: [CoreUnify]
subst evs :: [((EvTerm, Ct), [Ct])]
evs leqsG :: [(CoreSOP, CoreSOP, Bool)]
leqsG xs :: [(Either NatEquality NatInEquality, [(Type, Type)])]
xs (eq :: (Either NatEquality NatInEquality, [(Type, Type)])
eq@(Right (ct :: Ct
ct,u :: (CoreSOP, CoreSOP, Bool)
u@(x :: CoreSOP
x,y :: CoreSOP
y,b :: Bool
b)),k :: [(Type, Type)]
k):eqs' :: [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs') = do
      let u' :: CoreSOP
u'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst ((CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP, CoreSOP, Bool)
u)
          x' :: CoreSOP
x'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
x
          y' :: CoreSOP
y'    = [CoreUnify] -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [CoreUnify]
subst CoreSOP
y
          uS :: (CoreSOP, CoreSOP, Bool)
uS    = (CoreSOP
x',CoreSOP
y',Bool
b)
          leqsG' :: [(CoreSOP, CoreSOP, Bool)]
leqsG' | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = (CoreSOP
x',CoreSOP
y',Bool
b)(CoreSOP, CoreSOP, Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a. a -> [a] -> [a]
:[(CoreSOP, CoreSOP, Bool)]
leqsG
                 | Bool
otherwise               = [(CoreSOP, CoreSOP, Bool)]
leqsG
          ineqs :: [(CoreSOP, CoreSOP, Bool)]
ineqs = [[(CoreSOP, CoreSOP, Bool)]] -> [(CoreSOP, CoreSOP, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(CoreSOP, CoreSOP, Bool)]
leqsG
                         , ((CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool))
-> [(CoreSOP, CoreSOP, Bool)] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([CoreUnify] -> (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool)
forall v c c.
(Ord v, Ord c) =>
[UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq [CoreUnify]
subst) [(CoreSOP, CoreSOP, Bool)]
leqsG
                         , (NatInEquality -> (CoreSOP, CoreSOP, Bool))
-> [NatInEquality] -> [(CoreSOP, CoreSOP, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map NatInEquality -> (CoreSOP, CoreSOP, Bool)
forall a b. (a, b) -> b
snd ([Either NatEquality NatInEquality] -> [NatInEquality]
forall a b. [Either a b] -> [b]
rights (((Either NatEquality NatInEquality, [(Type, Type)])
 -> Either NatEquality NatInEquality)
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [Either NatEquality NatInEquality]
forall a b. (a -> b) -> [a] -> [b]
map (Either NatEquality NatInEquality, [(Type, Type)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst [(Either NatEquality NatInEquality, [(Type, Type)])]
eqsG))
                         ]
      [Char] -> SDoc -> TcPluginM ()
tcPluginTrace "unifyNats(ineq) results" ((Ct, (CoreSOP, CoreSOP, Bool), CoreSOP, [(CoreSOP, CoreSOP, Bool)])
-> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct
ct,(CoreSOP, CoreSOP, Bool)
u,CoreSOP
u',[(CoreSOP, CoreSOP, Bool)]
ineqs))
      case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
u') of
        Just (True,knW :: Set CType
knW)  -> do
          [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
knW ([(Type, Type)] -> [(Type, Type)]
subToPred [(Type, Type)]
k)
          [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'

        Just (False,_) -> SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NatEquality NatInEquality -> SimplifyResult
Impossible ((Either NatEquality NatInEquality, [(Type, Type)])
-> Either NatEquality NatInEquality
forall a b. (a, b) -> a
fst (Either NatEquality NatInEquality, [(Type, Type)])
eq))
        Nothing
          -- This inequality is either a given constraint, or it is a wanted
          -- constraint, which in normal form is equal to another given
          -- constraint, hence it can be solved.
          | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (((CoreSOP, CoreSOP, Bool) -> Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [Bool]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
u) [(CoreSOP, CoreSOP, Bool)]
ineqs) Bool -> Bool -> Bool
||
          -- Or the above, but with valid substitutions applied to the wanted.
            [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (((CoreSOP, CoreSOP, Bool) -> Maybe Bool)
-> [(CoreSOP, CoreSOP, Bool)] -> [Bool]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> Maybe Bool
solveIneq Word
depth (CoreSOP, CoreSOP, Bool)
uS) [(CoreSOP, CoreSOP, Bool)]
ineqs) Bool -> Bool -> Bool
||
          -- Or it is an inequality that can be instantly solved, such as
          -- `1 <= x^y`
            Word -> (CoreSOP, CoreSOP, Bool) -> Bool
instantSolveIneq Word
depth (CoreSOP, CoreSOP, Bool)
u
          -> do
            [((EvTerm, Ct), [Ct])]
evs' <- [((EvTerm, Ct), [Ct])]
-> (((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> Maybe ((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [((EvTerm, Ct), [Ct])]
evs (((EvTerm, Ct), [Ct])
-> [((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
forall a. a -> [a] -> [a]
:[((EvTerm, Ct), [Ct])]
evs) (Maybe ((EvTerm, Ct), [Ct]) -> [((EvTerm, Ct), [Ct])])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-> TcPluginM [((EvTerm, Ct), [Ct])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic Ct
ct Set CType
forall a. Set a
empty ([(Type, Type)] -> [(Type, Type)]
subToPred [(Type, Type)]
k)
            [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs' [(CoreSOP, CoreSOP, Bool)]
leqsG' [(Either NatEquality NatInEquality, [(Type, Type)])]
xs [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'
          | Bool
otherwise
          -> [CoreUnify]
-> [((EvTerm, Ct), [Ct])]
-> [(CoreSOP, CoreSOP, Bool)]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> TcPluginM SimplifyResult
simples [CoreUnify]
subst [((EvTerm, Ct), [Ct])]
evs [(CoreSOP, CoreSOP, Bool)]
leqsG ((Either NatEquality NatInEquality, [(Type, Type)])
eq(Either NatEquality NatInEquality, [(Type, Type)])
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
-> [(Either NatEquality NatInEquality, [(Type, Type)])]
forall a. a -> [a] -> [a]
:[(Either NatEquality NatInEquality, [(Type, Type)])]
xs) [(Either NatEquality NatInEquality, [(Type, Type)])]
eqs'

    eqToLeq :: a -> a -> [(a, a, Bool)]
eqToLeq x :: a
x y :: a
y = [(a
x,a
y,Bool
True),(a
y,a
x,Bool
True)]
    substLeq :: [UnifyItem v c] -> (SOP v c, SOP v c, c) -> (SOP v c, SOP v c, c)
substLeq s :: [UnifyItem v c]
s (x :: SOP v c
x,y :: SOP v c
y,b :: c
b) = ([UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
x, [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
y, c
b)

-- Extract the Nat equality constraints
toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
toNatEquality ct :: Ct
ct = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
    EqPred NomEq t1 :: Type
t1 t2 :: Type
t2
      -> Type
-> Type -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
go Type
t1 Type
t2
    _ -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
  where
    go :: Type
-> Type -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
go (TyConApp tc :: TyCon
tc xs :: [Type]
xs) (TyConApp tc' :: TyCon
tc' ys :: [Type]
ys)
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc'
      , [TyCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCon
tc,TyCon
tc'] [TyCon] -> [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TyCon
typeNatAddTyCon,TyCon
typeNatSubTyCon
                                   ,TyCon
typeNatMulTyCon,TyCon
typeNatExpTyCon])
      = case ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Type, Type) -> Bool) -> (Type, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
xs [Type]
ys) of
          [(x :: Type
x,y :: Type
y)]
            | Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
x)
            , Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
y)
            , let (x' :: CoreSOP
x',k1 :: [(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
            , let (y' :: CoreSOP
y',k2 :: [(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
            -> (Either NatEquality NatInEquality, [(Type, Type)])
-> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (Ct
ct, CoreSOP
x', CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
          _ -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatLeqTyCon
      , [x :: Type
x,y :: Type
y] <- [Type]
xs
      , let (x' :: CoreSOP
x',k1 :: [(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (y' :: CoreSOP
y',k2 :: [(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      , let ks :: [(Type, Type)]
ks      = [(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2
      = case TyCon
tc' of
         _ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
           -> (Either NatEquality NatInEquality, [(Type, Type)])
-> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
True)), [(Type, Type)]
ks)
         _ | TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
           -> (Either NatEquality NatInEquality, [(Type, Type)])
-> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct, (CoreSOP
x', CoreSOP
y', Bool
False)), [(Type, Type)]
ks)
         _ -> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing

    go x :: Type
x y :: Type
y
      | Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
x)
      , Type -> Bool
isNatKind (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
y)
      , let (x' :: CoreSOP
x',k1 :: [(Type, Type)]
k1) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x)
      , let (y' :: CoreSOP
y',k2 :: [(Type, Type)]
k2) = Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
      = (Either NatEquality NatInEquality, [(Type, Type)])
-> Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. a -> Maybe a
Just (NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (Ct
ct,CoreSOP
x',CoreSOP
y'),[(Type, Type)]
k1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
k2)
      | Bool
otherwise
      = Maybe (Either NatEquality NatInEquality, [(Type, Type)])
forall a. Maybe a
Nothing

    isNatKind :: Kind -> Bool
    isNatKind :: Type -> Bool
isNatKind = (Type -> Type -> Bool
`eqType` Type
typeNatKind)

unifyItemToPredType :: CoreUnify -> (PredType,Kind)
unifyItemToPredType :: CoreUnify -> (Type, Type)
unifyItemToPredType ui :: CoreUnify
ui =
    (Type -> Type -> Type
mkPrimEqPred Type
ty1 Type
ty2,Type
typeNatKind)
  where
    ty1 :: Type
ty1 = case CoreUnify
ui of
            SubstItem {..} -> TyVar -> Type
mkTyVarTy TyVar
siVar
            UnifyItem {..} -> CoreSOP -> Type
reifySOP CoreSOP
siLHS
    ty2 :: Type
ty2 = case CoreUnify
ui of
            SubstItem {..} -> CoreSOP -> Type
reifySOP CoreSOP
siSOP
            UnifyItem {..} -> CoreSOP -> Type
reifySOP CoreSOP
siRHS

evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic :: Ct
-> Set CType
-> [(Type, Type)]
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
evMagic ct :: Ct
ct knW :: Set CType
knW preds :: [(Type, Type)]
preds = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
  EqPred NomEq t1 :: Type
t1 t2 :: Type
t2 -> do
    let predTypes :: [Type]
predTypes = ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst [(Type, Type)]
preds
        predKinds :: [Type]
predKinds = ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> b
snd [(Type, Type)]
preds
#if MIN_VERSION_ghc(8,4,1)
    [CoercionHole]
holes <- (Type -> TcPluginM CoercionHole)
-> [Type] -> TcPluginM [CoercionHole]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> TcPluginM CoercionHole
newCoercionHole (Type -> TcPluginM CoercionHole)
-> (Type -> Type) -> Type -> TcPluginM CoercionHole
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Type) -> (Type, Type) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Type
mkPrimEqPred ((Type, Type) -> Type) -> (Type -> (Type, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, Type)
getEqPredTys) [Type]
predTypes
#else
    holes <- replicateM (length preds) newCoercionHole
#endif
    [Ct]
knWanted <- (CType -> TcPluginM Ct) -> [CType] -> TcPluginM [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Ct -> CType -> TcPluginM Ct
mkKnWanted Ct
ct) (Set CType -> [CType]
forall a. Set a -> [a]
toList Set CType
knW)
    let newWanted :: [Ct]
newWanted = [Ct]
knWanted [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ (Type -> CoercionHole -> Ct) -> [Type] -> [CoercionHole] -> [Ct]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (CtLoc -> Type -> CoercionHole -> Ct
unifyItemToCt (Ct -> CtLoc
ctLoc Ct
ct)) [Type]
predTypes [CoercionHole]
holes
        ctEv :: Coercion
ctEv      = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo ([Char] -> UnivCoProvenance
PluginProv "ghc-typelits-natnormalise") Role
Nominal Type
t1 Type
t2
#if MIN_VERSION_ghc(8,4,1)
        holeEvs :: [Coercion]
holeEvs   = (CoercionHole -> Coercion) -> [CoercionHole] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map CoercionHole -> Coercion
mkHoleCo [CoercionHole]
holes
#else
        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes predTypes
#endif
    Coercion
forallEv <- [(TyVar, Coercion)] -> Coercion -> Coercion
mkForAllCos ([(TyVar, Coercion)] -> Coercion -> Coercion)
-> TcPluginM [(TyVar, Coercion)]
-> TcPluginM (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> TcPluginM (TyVar, Coercion))
-> [Type] -> TcPluginM [(TyVar, Coercion)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TcPluginM (TyVar, Coercion)
mkCoVar [Type]
predKinds) TcPluginM (Coercion -> Coercion)
-> TcPluginM Coercion -> TcPluginM Coercion
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> TcPluginM Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
ctEv
    let finalEv :: Coercion
finalEv = (Coercion -> Coercion -> Coercion)
-> Coercion -> [Coercion] -> Coercion
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Coercion -> Coercion -> Coercion
mkInstCo Coercion
forallEv [Coercion]
holeEvs
#if MIN_VERSION_ghc(8,5,0)
    Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return (((EvTerm, Ct), [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
forall a. a -> Maybe a
Just ((EvExpr -> EvTerm
EvExpr (Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
finalEv), Ct
ct),[Ct]
newWanted))
#else
    return (Just ((EvCoercion finalEv, ct),newWanted))
#endif
  _ -> Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ((EvTerm, Ct), [Ct])
forall a. Maybe a
Nothing
  where
    mkCoVar :: Type -> TcPluginM (TyVar, Coercion)
mkCoVar k :: Type
k = (,Coercion
natReflCo) (TyVar -> (TyVar, Coercion))
-> TcPluginM TyVar -> TcPluginM (TyVar, Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> TcPluginM TyVar
newFlexiTyVar Type
k)
      where
        natReflCo :: Coercion
natReflCo = Type -> Coercion
mkNomReflCo Type
k

mkKnWanted
  :: Ct
  -> CType
  -> TcPluginM Ct
mkKnWanted :: Ct -> CType -> TcPluginM Ct
mkKnWanted ct :: Ct
ct (CType ty :: Type
ty) = do
  Class
kc_clas <- Name -> TcPluginM Class
tcLookupClass Name
knownNatClassName
  let kn_pred :: Type
kn_pred = Class -> [Type] -> Type
mkClassPred Class
kc_clas [Type
ty]
  CtEvidence
wantedCtEv <- CtLoc -> Type -> TcPluginM CtEvidence
TcPluginM.newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
kn_pred
  let wanted :: Ct
wanted = CtEvidence -> Ct
mkNonCanonical CtEvidence
wantedCtEv
      -- Set the source-location of the new wanted constraint to the source
      -- location of the [W]anted constraint we are currently trying to solve
      ct_ls :: RealSrcSpan
ct_ls   = CtLoc -> RealSrcSpan
ctLocSpan (Ct -> CtLoc
ctLoc Ct
ct)
      ctl :: CtLoc
ctl     = CtEvidence -> CtLoc
ctEvLoc  CtEvidence
wantedCtEv
      wanted' :: Ct
wanted' = Ct -> CtLoc -> Ct
setCtLoc Ct
wanted (CtLoc -> RealSrcSpan -> CtLoc
setCtLocSpan CtLoc
ctl RealSrcSpan
ct_ls)
  Ct -> TcPluginM Ct
forall (m :: * -> *) a. Monad m => a -> m a
return Ct
wanted'

unifyItemToCt :: CtLoc
              -> PredType
              -> CoercionHole
              -> Ct
unifyItemToCt :: CtLoc -> Type -> CoercionHole -> Ct
unifyItemToCt loc :: CtLoc
loc pred_type :: Type
pred_type hole :: CoercionHole
hole =
  CtEvidence -> Ct
mkNonCanonical
    (Type -> TcEvDest -> ShadowInfo -> CtLoc -> CtEvidence
CtWanted
      Type
pred_type
      (CoercionHole -> TcEvDest
HoleDest CoercionHole
hole)
#if MIN_VERSION_ghc(8,2,0)
      ShadowInfo
WDeriv
#endif
      CtLoc
loc)