ghc-typelits-natnormalise 0.7.12 → 0.8.0

raw patch · 11 files changed

+1403/−2577 lines, 11 filesdep +ghc-tcplugin-apidep −ghc-tcplugins-extradep ~ghcdep ~ghc-bignumdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-tcplugin-api

Dependencies removed: ghc-tcplugins-extra

Dependency ranges changed: ghc, ghc-bignum, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• ghc-typelits-natnormalise.cabal +19/−18
• src-ghc-9.12/GHC/TypeLits/Normalise.hs +0/−739
• src-ghc-9.4/GHC/TypeLits/Normalise.hs +0/−740
• src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs +0/−862
• src/GHC/TypeLits/Normalise.hs +731/−0
• src/GHC/TypeLits/Normalise/Compat.hs +381/−0
• src/GHC/TypeLits/Normalise/SOP.hs +20/−19
• src/GHC/TypeLits/Normalise/Unify.hs +198/−193
• tests/ErrorTests.hs +8/−5
• tests/Tests.hs +39/−1

@@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.8 *September 8th 2025*+* Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier+* Support for GHC versions older than 8.8 is dropped+* Fixes [#70](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70) The constraint 0 < d+1 does not seem to resolve?+* Fixes [#71](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71) "Could not deduce ... from the context ...", but if the context removed, deduced outright+* Fixes [#47](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/47) Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)`+ ## 0.7.12 *August 22nd 2025* * Support for GHC 9.10.2 

@@ -1,5 +1,6 @@+cabal-version:       3.0 name:                ghc-typelits-natnormalise-version:             0.7.12+version:             0.8.0 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -37,7 +38,7 @@   Pragma to the header of your file. homepage:            http://www.clash-lang.org/ bug-reports:         http://github.com/clash-lang/ghc-typelits-natnormalise/issues-license:             BSD2+license:             BSD-2-Clause license-file:        LICENSE author:              Christiaan Baaij maintainer:          christiaan.baaij@gmail.com@@ -47,11 +48,9 @@ build-type:          Simple extra-source-files:  README.md                      CHANGELOG.md-cabal-version:       >=1.10-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,-                     GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,-                     GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1,-                     GHC == 9.10.2, GHC == 9.12.1+tested-with:         GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+                     GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, GHC == 9.10.2,+                     GHC == 9.12.2  source-repository head   type: git@@ -67,24 +66,26 @@   exposed-modules:     GHC.TypeLits.Normalise,                        GHC.TypeLits.Normalise.SOP,                        GHC.TypeLits.Normalise.Unify+  other-modules:       GHC.TypeLits.Normalise.Compat   build-depends:       base                >=4.9   && <5,                        containers          >=0.5.7.1 && <0.8,-                       ghc                 >=8.0.1 && <9.13,-                       ghc-tcplugins-extra >=0.5,+                       ghc                 >=8.8.1 && <9.15,+                       ghc-tcplugin-api    >=0.17.0 && <0.18,                        transformers        >=0.5.2.0 && < 0.7   if impl(ghc >= 9.0.0)-    build-depends:     ghc-bignum >=1.0 && <1.4+    build-depends:     ghc-bignum >=1.0 && <1.5   else     build-depends:     integer-gmp >=1.0 && <1.1++    mixins:+      ghc+        ( TcTypeNats as GHC.Builtin.Types.Literals+        , TyCon      as GHC.Core.TyCon+        , TysWiredIn as GHC.Builtin.Types+        , Unique     as GHC.Types.Unique+        )+   hs-source-dirs:      src-  if impl(ghc >= 8.0) && impl(ghc < 9.4)-    hs-source-dirs:    src-pre-ghc-9.4-  if impl(ghc >= 9.4) && impl(ghc < 9.11)-    hs-source-dirs:    src-ghc-9.4-    build-depends:     template-haskell    >=2.17 && <2.23-  if impl(ghc >= 9.11) && impl(ghc < 9.13)-    hs-source-dirs:    src-ghc-9.12-    build-depends:     template-haskell    >=2.17 && <2.24   default-language:    Haskell2010   other-extensions:    CPP                        LambdaCase

@@ -1,739 +0,0 @@-{-|-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 LambdaCase      #-}-{-# LANGUAGE NamedFieldPuns  #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections   #-}-{-# LANGUAGE ViewPatterns    #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise-  ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad ((<=<), forM)-import Control.Monad.Trans.Writer.Strict-import Data.Either (partitionEithers, rights)-import Data.IORef-import Data.List (intersect, partition, stripPrefix, find)-import Data.Maybe (mapMaybe, catMaybes)-import Data.Set (Set, empty, toList, notMember, fromList, union)-import Text.Read (readMaybe)-import qualified Data.Type.Ord-import qualified GHC.TypeError--import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)---- GHC API-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals-  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (Coercion, Role (..), mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate-  (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,-   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.Type-  (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-import GHC.Core.TyCo.Compare-  (eqType)-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))-import GHC.Tc.Plugin-  (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)-import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))-import GHC.Tc.Types.Constraint-  (Ct, CtEvidence (..), TcEvDest (..), ctEvidence, ctEvCoercion, ctLoc, isGiven,-   isWanted, mkNonCanonical, isWantedCt, ctEvLoc, ctEvPred, ctEvExpr,-   emptyRewriterSet, setCtEvLoc)-import GHC.Tc.Types.CtLoc (CtLoc, ctLocSpan, setCtLocSpan)-import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId, mkEvCast)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of-  Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey-  _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin-  = defaultPlugin-  { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument-  , pluginRecompile = purePlugin-  }- where-  parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })-  parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })-  parseArgument _ = Nothing-  defaultOpts = Opts { negNumbers = False, depth = 5 }--data Opts = Opts { negNumbers :: Bool, depth :: Word }--normalisePlugin :: Opts -> TcPlugin-normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise"-  TcPlugin { tcPluginInit    = lookupExtraDefs-           , tcPluginSolve   = decideEqualSOP opts-           , tcPluginRewrite = const emptyUFM-           , tcPluginStop    = const (return ())-           }--type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do-    ref <- tcPluginIO (newIORef empty)-    ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon-    leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon-    assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon-    return (ref, (leqT,assertT,ordCond))--lookupTHName :: TH.Name -> TcPluginM Name-lookupTHName th = do-    nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)-    res <- tcPluginIO $ thNameToGhcNameIO nc th-    maybe (fail $ "Failed to lookup " ++ show th) return res--decideEqualSOP-  :: Opts-  -> ExtraDefs-      -- ^ 1. Givens that is already generated.-      --   We have to generate new givens at most once;-      --   otherwise GHC will loop indefinitely.-      ---      ---      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond-      --      For older: TyCon of GHC.TypeLits.<=?-  -> EvBindsVar-  -> [Ct]-  -> [Ct]-  -> TcPluginM TcPluginSolveResult---- Simplification phase: Derives /simplified/ givens;--- we can reduce given constraints like @Show (Foo (n + 2))@--- to its normal form @Show (Foo (2 + n))@, which is eventually--- useful in solving phase.------ This helps us to solve /indirect/ constraints;--- without this phase, we cannot derive, e.g.,--- @IsVector UVector (Fin (n + 1))@ from--- @Unbox (1 + n)@!-decideEqualSOP opts (gen'd,(leqT,_,_)) ev givens [] = do-    done <- tcPluginIO $ readIORef gen'd-    let reds =-          filter (\(_,(_,_,v)) -> null v || negNumbers opts) $-          reduceGivens opts leqT done givens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds-    tcPluginIO $-      modifyIORef' gen'd $ union (fromList newlyDone)-    newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm-    return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do-    let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds-        nonEqs = filter ( not-                        . (\p -> isEqPred p || isEqPrimPred p)-                        . ctEvPred-                        . ctEvidence )-                 wanteds-    done <- tcPluginIO $ readIORef gen'd-    let redGs = reduceGivens opts leqT done givens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs-    redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm-    reducible_wanteds-      <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>-                                    reduceNatConstr (givens ++ redGivens) ct)-                            nonEqs-    if null unit_wanteds && null reducible_wanteds-    then return $ TcPluginOk [] []-    else do-        -- Since reducible wanteds also can have some negation/subtraction-        -- subterms, we have to make sure appropriate inequalities to hold.-        -- Here, we generate such additional inequalities for reduction-        -- that is to be added to new [W]anteds.-        ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $-          fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)-        tcPluginIO $-          modifyIORef' gen'd $ union (fromList newlyDone)-        let unit_givens = mapMaybe-                            (toNatEquality tcs)-                            givens-        sr <- simplifyNats opts leqT unit_givens unit_wanteds-        tcPluginTrace "normalised" (ppr sr)-        reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do-          wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws-          return ((term, origCt), wDicts ++ wants)-        case sr of-          Simplified evs -> do-            let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs-                -- Only solve derived when we solved a wanted-                simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of-                            [] -> []-                            _  -> simpld-                (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)-            return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)-          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality   = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts leqT done givens =-  let nonEqs =-        [ ct-        | ct <- givens-        , let ev = ctEvidence ct-              prd = ctEvPred ev-        , isGiven ev-        , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd-        ]-  in filter-      (\(_, (prd, _, _)) ->-        notMember (CType prd) done-      )-    $ mapMaybe-      (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct)-      nonEqs--tryReduceGiven-  :: Opts -> TyCon -> [Ct] -> Ct-  -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts leqT simplGivens ct = do-    let (mans, ws) =-          runWriter $ normaliseNatEverywhere $-          ctEvPred $ ctEvidence ct-        ws' = [ p-              | p <- subToPred opts leqT ws-              , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens-              ]-        -- deps = unitDVarSet (ctEvId ct)-    pred' <- mans-    return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left  (ct, _, _)) = ct-fromNatEquality (Right (ct, _))    = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct =  do-  let pred0 = ctEvPred $ ctEvidence ct-      (mans, tests) = runWriter $ normaliseNatEverywhere pred0-  case mans of-    Nothing -> return Nothing-    Just pred' -> do-      case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of-        -- No existing evidence found-        Nothing -> case getClassPredTys_maybe pred' of-          -- Are we trying to solve a class instance?-          Just (cls,_) | className cls /= knownNatClassName -> do-            -- Create new evidence binding for normalized class constraint-            evVar <- newEvVar pred'-            -- Bind the evidence to a new wanted normalized class constraint-            let wDict = mkNonCanonical-                          (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)-            -- Evidence for current wanted is simply the coerced binding for-            -- the new binding-                evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []-                         Representational-                         pred' pred0-                ev = mkEvCast (evId evVar) evCo-            -- Use newly created coerced wanted as evidence, and emit the-            -- normalized wanted as a new constraint to solve.-            return (Just (ev, tests, [wDict]))-          _ -> return Nothing-        -- Use existing evidence-        Just c  -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =-  let pred0 = ctEvPred ct-      evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []-              Representational-              pred0 pred'-      ev = mkEvCast (ctEvExpr ct) evCo-  in ev--data SimplifyResult-  = Simplified [((EvTerm,Ct),[Ct])]-  | Impossible (Either NatEquality NatInEquality)--instance Outputable SimplifyResult where-  ppr (Simplified evs) = text "Simplified" $$ ppr evs-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq--simplifyNats-  :: Opts-  -- ^ Allow negated numbers (potentially unsound!)-  -> TyCon-  -- * TyCon of Data.Type.Ord.<=-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Given constraints-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Wanted constraints-  -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} leqT eqsG eqsW = do-    let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG-        (varEqs,otherEqs) = partition isVarEqs eqsG1-        fancyGivens = concatMap (makeGivensSet otherEqs) varEqs-    case varEqs of-      [] -> do-        let eqs = otherEqs ++ eqsW-        tcPluginTrace "simplifyNats" (ppr eqs)-        simples [] [] [] [] [] eqs-      _  -> do-        tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")-                      (ppr varEqs)--        allSimplified <- forM fancyGivens $ \v -> do-          let eqs = v ++ eqsW-          tcPluginTrace "simplifyNats" (ppr eqs)-          simples [] [] [] [] [] eqs--        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)-  where-    simples :: [Coercion]-            -> [CoreUnify]-            -> [((EvTerm, Ct), [Ct])]-            -> [(CoreSOP,CoreSOP,Bool)]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> TcPluginM SimplifyResult-    simples _ _subst evs _leqsG _xs [] = return (Simplified evs)-    simples deps subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do-      let u' = substsSOP subst u-          v' = substsSOP subst v-      ur <- unifyNats ct u' v'-      tcPluginTrace "unifyNats result" (ppr ur)-      case ur of-        Win -> do-          evs' <- maybe evs (:evs) <$> evMagic ct deps empty (subToPred opts leqT k)-          simples deps subst evs' leqsG [] (xs ++ eqs')-        Lose -> if null evs && null eqs'-                   then return (Impossible (fst eq))-                   else simples deps subst evs leqsG xs eqs'-        Draw [] -> simples deps subst evs [] (eq:xs) eqs'-        Draw subst' -> do-          evM <- evMagic ct deps empty (map unifyItemToPredType subst' ++-                                        subToPred opts leqT k)-          let (leqsG1, deps1)-                | isGiven (ctEvidence ct) = ( eqToLeq u' v' ++ leqsG-                                            , ctEvCoercion (ctEvidence ct):deps)-                | otherwise               = (leqsG, deps)-          case evM of-            Nothing -> simples deps1 subst evs leqsG1 xs eqs'-            Just ev ->-              simples (ctEvCoercion (ctEvidence ct):deps)-                      (substsSubst subst' subst ++ subst')-                      (ev:evs) leqsG1 [] (xs ++ eqs')-    simples deps subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do-      let u'    = substsSOP subst (subtractIneq u)-          x'    = substsSOP subst x-          y'    = substsSOP subst y-          uS    = (x',y',b)-          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG-                 | otherwise               = leqsG-          ineqs = concat [ leqsG-                         , map (substLeq subst) leqsG-                         , map snd (rights (map fst eqsG))-                         ]-      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))-      case runWriterT (isNatural u') of-        Just (True,knW)  -> do-          evs' <- maybe evs (:evs) <$> evMagic ct deps knW (subToPred opts leqT k)-          simples deps subst evs' leqsG' xs eqs'--        Just (False,_) | null k -> return (Impossible (fst eq))-        _ -> do-          let solvedIneq = mapMaybe runWriterT-                 -- it is an inequality that can be instantly solved, such as-                 -- `1 <= x^y`-                 -- OR-                (instantSolveIneq depth u:-                instantSolveIneq depth uS:-                -- 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.-                -- OR-                map (solveIneq depth u) ineqs ++-                -- The above, but with valid substitutions applied to the wanted.-                map (solveIneq depth uS) ineqs)-              smallest = solvedInEqSmallestConstraint solvedIneq-          case smallest of-            (True,kW) -> do-              evs' <- maybe evs (:evs) <$> evMagic ct deps kW (subToPred opts leqT k)-              simples deps subst evs' leqsG' xs eqs'-            _ -> simples deps subst evs leqsG (eq:xs) eqs'--    eqToLeq x y = [(x,y,True),(y,x,True)]-    substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)--    isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True-    isVarEqs _ = False--    makeGivensSet otherEqs varEq-      = let (noMentionsV,mentionsV)   = partitionEithers-                                          (map (matchesVarEq varEq) otherEqs)-            (mentionsLHS,mentionsRHS) = partitionEithers mentionsV-            vS = swapVar varEq-            givensLHS = case mentionsLHS of-              [] -> []-              _  -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]-            givensRHS = case mentionsRHS of-              [] -> []-              _  -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]-        in  case mentionsV of-              [] -> [noMentionsV]-              _  -> givensLHS ++ givensRHS--    matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of-      (Left (_,S [P [V v3]],_),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Left (_,_,S [P [V v3]]),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(S [P [V v3]],_,_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(_,S [P [V v3]],_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      _ -> Left r-    matchesVarEq _ _ = error "internal error"--    swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) =-      (Left (ct,S [P [V v2]], S [P [V v1]]),ps)-    swapVar _ = error "internal error"--    findFirstSimpliedWanted (Impossible e)   _  = Impossible e-    findFirstSimpliedWanted (Simplified evs) s2-      | any (isWantedCt . snd . fst) evs-      = Simplified evs-      | otherwise-      = s2---- 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 :: Opts -> TyCon -> [(Type, Type)] -> [PredType]-subToPred Opts{..} leqT-  | negNumbers = const []-  | otherwise  = map leq-  where-    leq (a,b) =-      let lhs = TyConApp leqT [naturalTy,b,a]-          rhs = TyConApp (cTupleTyCon 0) []-       in mkPrimEqPred lhs rhs---- Extract the Nat equality constraints-toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2-      -> go t1 t2-    IrredPred p-      -> go2 p-    _ -> Nothing-  where-    go (TyConApp tc xs) (TyConApp tc' ys)-      | tc == tc'-      , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon-                                   ,typeNatMulTyCon,typeNatExpTyCon])-      = case filter (not . uncurry eqType) (zip xs ys) of-          [(x,y)]-            | isNatKind (typeKind x)-            , isNatKind (typeKind y)-            , let (x',k1) = runWriter (normaliseNat x)-            , let (y',k2) = runWriter (normaliseNat y)-            -> Just (Left (ct, x', y'),k1 ++ k2)-          _ -> Nothing-      | tc == ordCond-      , [_,cmp,lt,eq,gt] <- xs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = case tc' of-         _ | tc' == promotedTrueDataCon-           -> Just (Right (ct, (x', y', True)), ks)-         _ | tc' == promotedFalseDataCon-           -> Just (Right (ct, (x', y', False)), ks)-         _ -> Nothing-      | tc == assertT-      , tc' == (cTupleTyCon 0)-      , [] <- ys-      , [TyConApp ordCondTc zs, _] <- xs-      , ordCondTc == ordCond-      , [_,cmp,lt,eq,gt] <- zs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = Just (Right (ct, (x', y', True)), ks)--    go x y-      | isNatKind (typeKind x)-      , isNatKind (typeKind y)-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      = Just (Left (ct,x',y'),k1 ++ k2)-      | otherwise-      = Nothing--    go2 (TyConApp tc ys)-      | tc == assertT-      , [TyConApp ordCondTc xs, _] <- ys-      , ordCondTc == ordCond-      , [_,cmp,lt,eq,gt] <- xs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = Just (Right (ct, (x', y', True)), ks)--    go2 _ = Nothing--    isNatKind :: Kind -> Bool-    isNatKind = (`eqType` naturalTy)--unifyItemToPredType :: CoreUnify -> PredType-unifyItemToPredType ui = mkPrimEqPred ty1 ty2-  where-    ty1 = case ui of-            SubstItem {..} -> mkTyVarTy siVar-            UnifyItem {..} -> reifySOP siLHS-    ty2 = case ui of-            SubstItem {..} -> reifySOP siSOP-            UnifyItem {..} -> reifySOP siRHS--evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]-evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)--evMagic :: Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct deps knW preds = do-  holeWanteds <- evSubtPreds (ctLoc ct) preds-  knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)-  let newWant = knWanted ++ holeWanteds-  case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2 ->-      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Nominal t1 t2-      in return (Just ((EvExpr (Coercion ctEv), ct),newWant))-    IrredPred p ->-      let t1 = mkTyConApp (cTupleTyCon 0) []-          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Representational t1 p-          dcApp = evId (dataConWrapId (cTupleDataCon 0))-       in return (Just ((evCast dcApp co, ct),newWant))-    _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =-  let ct_ls   = ctLocSpan origCtl-      ctl     = ctEvLoc  ev-  in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls))--mkKnWanted-  :: CtLoc-  -> CType-  -> TcPluginM Ct-mkKnWanted loc (CType ty) = do-  kc_clas <- tcLookupClass knownNatClassName-  let kn_pred = mkClassPred kc_clas [ty]-  wantedCtEv <- newWanted loc kn_pred-  let wanted' = mkNonCanonical' loc wantedCtEv-  return wanted'

@@ -1,740 +0,0 @@-{-|-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 NamedFieldPuns  #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections   #-}-{-# LANGUAGE ViewPatterns    #-}-{-# LANGUAGE TemplateHaskellQuotes #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise-  ( plugin )-where---- external-import Control.Arrow (second)-import Control.Monad ((<=<), forM)-import Control.Monad.Trans.Writer.Strict-import Data.Either (partitionEithers, rights)-import Data.IORef-import Data.List (intersect, partition, stripPrefix, find)-import Data.Maybe (mapMaybe, catMaybes)-import Data.Set (Set, empty, toList, notMember, fromList, union)-import Text.Read (readMaybe)-import qualified Data.Type.Ord-import qualified GHC.TypeError--import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)---- GHC API-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals-  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (naturalTy, cTupleDataCon, cTupleTyCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (Role (..), mkUnivCo)-import GHC.Core.DataCon (dataConWrapId)-import GHC.Core.Predicate-  (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,-   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type-  (Kind, PredType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-import GHC.Core.TyCo.Compare-  (eqType)-#else-import GHC.Core.Type-  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)-#endif-import GHC.Data.IOEnv (getEnv)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))-import GHC.Tc.Plugin-  (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)-import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)-import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))-import GHC.Tc.Types.Constraint-  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence,-   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan,-   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc)-import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-import GHC (Name)---- template-haskell-import qualified Language.Haskell.TH as TH---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of-  Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey-  _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin-  = defaultPlugin-  { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument-  , pluginRecompile = purePlugin-  }- where-  parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })-  parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })-  parseArgument _ = Nothing-  defaultOpts = Opts { negNumbers = False, depth = 5 }--data Opts = Opts { negNumbers :: Bool, depth :: Word }--normalisePlugin :: Opts -> TcPlugin-normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise"-  TcPlugin { tcPluginInit    = lookupExtraDefs-           , tcPluginSolve   = decideEqualSOP opts-           , tcPluginRewrite = const emptyUFM-           , tcPluginStop    = const (return ())-           }--type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do-    ref <- tcPluginIO (newIORef empty)-    ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon-    leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon-    assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon-    return (ref, (leqT,assertT,ordCond))--lookupTHName :: TH.Name -> TcPluginM Name-lookupTHName th = do-    nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)-    res <- tcPluginIO $ thNameToGhcNameIO nc th-    maybe (fail $ "Failed to lookup " ++ show th) return res--decideEqualSOP-  :: Opts-  -> ExtraDefs-      -- ^ 1. Givens that is already generated.-      --   We have to generate new givens at most once;-      --   otherwise GHC will loop indefinitely.-      ---      ---      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond-      --      For older: TyCon of GHC.TypeLits.<=?-  -> EvBindsVar-  -> [Ct]-  -> [Ct]-  -> TcPluginM TcPluginSolveResult---- Simplification phase: Derives /simplified/ givens;--- we can reduce given constraints like @Show (Foo (n + 2))@--- to its normal form @Show (Foo (2 + n))@, which is eventually--- useful in solving phase.------ This helps us to solve /indirect/ constraints;--- without this phase, we cannot derive, e.g.,--- @IsVector UVector (Fin (n + 1))@ from--- @Unbox (1 + n)@!-decideEqualSOP opts (gen'd,(leqT,_,_)) ev givens [] = do-    done <- tcPluginIO $ readIORef gen'd-    let reds =-          filter (\(_,(_,_,v)) -> null v || negNumbers opts) $-          reduceGivens opts leqT done givens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds-    tcPluginIO $-      modifyIORef' gen'd $ union (fromList newlyDone)-    newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm-    return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do-    let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds-        nonEqs = filter ( not-                        . (\p -> isEqPred p || isEqPrimPred p)-                        . ctEvPred-                        . ctEvidence )-                 wanteds-    done <- tcPluginIO $ readIORef gen'd-    let redGs = reduceGivens opts leqT done givens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs-    redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven ev (ctLoc origCt) pred' evTerm-    reducible_wanteds-      <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>-                                    reduceNatConstr (givens ++ redGivens) ct)-                            nonEqs-    if null unit_wanteds && null reducible_wanteds-    then return $ TcPluginOk [] []-    else do-        -- Since reducible wanteds also can have some negation/subtraction-        -- subterms, we have to make sure appropriate inequalities to hold.-        -- Here, we generate such additional inequalities for reduction-        -- that is to be added to new [W]anteds.-        ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $-          fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)-        tcPluginIO $-          modifyIORef' gen'd $ union (fromList newlyDone)-        let unit_givens = mapMaybe-                            (toNatEquality tcs)-                            givens-        sr <- simplifyNats opts leqT unit_givens unit_wanteds-        tcPluginTrace "normalised" (ppr sr)-        reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do-          wants <- evSubtPreds (ctLoc origCt) $ subToPred opts leqT ws-          return ((term, origCt), wDicts ++ wants)-        case sr of-          Simplified evs -> do-            let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs-                -- Only solve derived when we solved a wanted-                simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of-                            [] -> []-                            _  -> simpld-                (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)-            return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)-          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality   = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts leqT done givens =-  let nonEqs =-        [ ct-        | ct <- givens-        , let ev = ctEvidence ct-              prd = ctEvPred ev-        , isGiven ev-        , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd-        ]-  in filter-      (\(_, (prd, _, _)) ->-        notMember (CType prd) done-      )-    $ mapMaybe-      (\ct -> (ct,) <$> tryReduceGiven opts leqT givens ct)-      nonEqs--tryReduceGiven-  :: Opts -> TyCon -> [Ct] -> Ct-  -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts leqT simplGivens ct = do-    let (mans, ws) =-          runWriter $ normaliseNatEverywhere $-          ctEvPred $ ctEvidence ct-        ws' = [ p-              | p <- subToPred opts leqT ws-              , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens-              ]-    pred' <- mans-    return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left  (ct, _, _)) = ct-fromNatEquality (Right (ct, _))    = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct =  do-  let pred0 = ctEvPred $ ctEvidence ct-      (mans, tests) = runWriter $ normaliseNatEverywhere pred0-  case mans of-    Nothing -> return Nothing-    Just pred' -> do-      case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of-        -- No existing evidence found-        Nothing -> case getClassPredTys_maybe pred' of-          -- Are we trying to solve a class instance?-          Just (cls,_) | className cls /= knownNatClassName -> do-            -- Create new evidence binding for normalized class constraint-            evVar <- newEvVar pred'-            -- Bind the evidence to a new wanted normalized class constraint-            let wDict = mkNonCanonical-                          (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)-            -- Evidence for current wanted is simply the coerced binding for-            -- the new binding-                evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")-                         Representational-                         pred' pred0-                ev = evId evVar `evCast` evCo-            -- Use newly created coerced wanted as evidence, and emit the-            -- normalized wanted as a new constraint to solve.-            return (Just (ev, tests, [wDict]))-          _ -> return Nothing-        -- Use existing evidence-        Just c  -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =-  let pred0 = ctEvPred ct-      evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")-              Representational-              pred0 pred'-      ev = ctEvExpr ct-             `evCast` evCo-  in ev--data SimplifyResult-  = Simplified [((EvTerm,Ct),[Ct])]-  | Impossible (Either NatEquality NatInEquality)--instance Outputable SimplifyResult where-  ppr (Simplified evs) = text "Simplified" $$ ppr evs-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq--simplifyNats-  :: Opts-  -- ^ Allow negated numbers (potentially unsound!)-  -> TyCon-  -- * TyCon of Data.Type.Ord.<=-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Given constraints-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Wanted constraints-  -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} leqT eqsG eqsW = do-    let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG-        (varEqs,otherEqs) = partition isVarEqs eqsG1-        fancyGivens = concatMap (makeGivensSet otherEqs) varEqs-    case varEqs of-      [] -> do-        let eqs = otherEqs ++ eqsW-        tcPluginTrace "simplifyNats" (ppr eqs)-        simples [] [] [] [] eqs-      _  -> do-        tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")-                      (ppr varEqs)--        allSimplified <- forM fancyGivens $ \v -> do-          let eqs = v ++ eqsW-          tcPluginTrace "simplifyNats" (ppr eqs)-          simples [] [] [] [] eqs--        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)-  where-    simples :: [CoreUnify]-            -> [((EvTerm, Ct), [Ct])]-            -> [(CoreSOP,CoreSOP,Bool)]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> TcPluginM SimplifyResult-    simples _subst evs _leqsG _xs [] = return (Simplified evs)-    simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do-      let u' = substsSOP subst u-          v' = substsSOP subst v-      ur <- unifyNats ct u' v'-      tcPluginTrace "unifyNats result" (ppr ur)-      case ur of-        Win -> do-          evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts leqT k)-          simples subst evs' leqsG [] (xs ++ eqs')-        Lose -> if null evs && null eqs'-                   then return (Impossible (fst eq))-                   else simples subst evs leqsG xs eqs'-        Draw [] -> simples subst evs [] (eq:xs) eqs'-        Draw subst' -> do-          evM <- evMagic ct empty (map unifyItemToPredType subst' ++-                                   subToPred opts leqT k)-          let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG-                     | otherwise  = leqsG-          case evM of-            Nothing -> simples subst evs leqsG' xs eqs'-            Just ev ->-              simples (substsSubst subst' subst ++ subst')-                      (ev:evs) leqsG' [] (xs ++ eqs')-    simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do-      let u'    = substsSOP subst (subtractIneq u)-          x'    = substsSOP subst x-          y'    = substsSOP subst y-          uS    = (x',y',b)-          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG-                 | otherwise               = leqsG-          ineqs = concat [ leqsG-                         , map (substLeq subst) leqsG-                         , map snd (rights (map fst eqsG))-                         ]-      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))-      case runWriterT (isNatural u') of-        Just (True,knW)  -> do-          evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts leqT k)-          simples subst evs' leqsG' xs eqs'--        Just (False,_) | null k -> return (Impossible (fst eq))-        _ -> do-          let solvedIneq = mapMaybe runWriterT-                 -- it is an inequality that can be instantly solved, such as-                 -- `1 <= x^y`-                 -- OR-                (instantSolveIneq depth u:-                instantSolveIneq depth uS:-                -- 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.-                -- OR-                map (solveIneq depth u) ineqs ++-                -- The above, but with valid substitutions applied to the wanted.-                map (solveIneq depth uS) ineqs)-              smallest = solvedInEqSmallestConstraint solvedIneq-          case smallest of-            (True,kW) -> do-              evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts leqT k)-              simples subst evs' leqsG' xs eqs'-            _ -> simples subst evs leqsG (eq:xs) eqs'--    eqToLeq x y = [(x,y,True),(y,x,True)]-    substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)--    isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True-    isVarEqs _ = False--    makeGivensSet otherEqs varEq-      = let (noMentionsV,mentionsV)   = partitionEithers-                                          (map (matchesVarEq varEq) otherEqs)-            (mentionsLHS,mentionsRHS) = partitionEithers mentionsV-            vS = swapVar varEq-            givensLHS = case mentionsLHS of-              [] -> []-              _  -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]-            givensRHS = case mentionsRHS of-              [] -> []-              _  -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]-        in  case mentionsV of-              [] -> [noMentionsV]-              _  -> givensLHS ++ givensRHS--    matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of-      (Left (_,S [P [V v3]],_),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Left (_,_,S [P [V v3]]),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(S [P [V v3]],_,_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(_,S [P [V v3]],_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      _ -> Left r-    matchesVarEq _ _ = error "internal error"--    swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) =-      (Left (ct,S [P [V v2]], S [P [V v1]]),ps)-    swapVar _ = error "internal error"--    findFirstSimpliedWanted (Impossible e)   _  = Impossible e-    findFirstSimpliedWanted (Simplified evs) s2-      | any (isWantedCt . snd . fst) evs-      = Simplified evs-      | otherwise-      = s2---- 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 :: Opts -> TyCon -> [(Type, Type)] -> [PredType]-subToPred Opts{..} leqT-  | negNumbers = const []-  | otherwise  = map leq-  where-    leq (a,b) =-      let lhs = TyConApp leqT [naturalTy,b,a]-          rhs = TyConApp (cTupleTyCon 0) []-       in mkPrimEqPred lhs rhs---- Extract the Nat equality constraints-toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality (_,assertT,ordCond) ct = case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2-      -> go t1 t2-    IrredPred p-      -> go2 p-    _ -> Nothing-  where-    go (TyConApp tc xs) (TyConApp tc' ys)-      | tc == tc'-      , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon-                                   ,typeNatMulTyCon,typeNatExpTyCon])-      = case filter (not . uncurry eqType) (zip xs ys) of-          [(x,y)]-            | isNatKind (typeKind x)-            , isNatKind (typeKind y)-            , let (x',k1) = runWriter (normaliseNat x)-            , let (y',k2) = runWriter (normaliseNat y)-            -> Just (Left (ct, x', y'),k1 ++ k2)-          _ -> Nothing-      | tc == ordCond-      , [_,cmp,lt,eq,gt] <- xs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = case tc' of-         _ | tc' == promotedTrueDataCon-           -> Just (Right (ct, (x', y', True)), ks)-         _ | tc' == promotedFalseDataCon-           -> Just (Right (ct, (x', y', False)), ks)-         _ -> Nothing-      | tc == assertT-      , tc' == (cTupleTyCon 0)-      , [] <- ys-      , [TyConApp ordCondTc zs, _] <- xs-      , ordCondTc == ordCond-      , [_,cmp,lt,eq,gt] <- zs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = Just (Right (ct, (x', y', True)), ks)--    go x y-      | isNatKind (typeKind x)-      , isNatKind (typeKind y)-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      = Just (Left (ct,x',y'),k1 ++ k2)-      | otherwise-      = Nothing--    go2 (TyConApp tc ys)-      | tc == assertT-      , [TyConApp ordCondTc xs, _] <- ys-      , ordCondTc == ordCond-      , [_,cmp,lt,eq,gt] <- xs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = Just (Right (ct, (x', y', True)), ks)--    go2 _ = Nothing--    isNatKind :: Kind -> Bool-    isNatKind = (`eqType` naturalTy)--unifyItemToPredType :: CoreUnify -> PredType-unifyItemToPredType ui = mkPrimEqPred ty1 ty2-  where-    ty1 = case ui of-            SubstItem {..} -> mkTyVarTy siVar-            UnifyItem {..} -> reifySOP siLHS-    ty2 = case ui of-            SubstItem {..} -> reifySOP siSOP-            UnifyItem {..} -> reifySOP siRHS--evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]-evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)--evMagic :: Ct -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct knW preds = do-  holeWanteds <- evSubtPreds (ctLoc ct) preds-  knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)-  let newWant = knWanted ++ holeWanteds-  case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2 ->-      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2-      in return (Just ((EvExpr (Coercion ctEv), ct),newWant))-    IrredPred p ->-      let t1 = mkTyConApp (cTupleTyCon 0) []-          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Representational t1 p-          dcApp = evId (dataConWrapId (cTupleDataCon 0))-       in return (Just ((evCast dcApp co, ct),newWant))-    _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =-  let ct_ls   = ctLocSpan origCtl-      ctl     = ctEvLoc  ev-  in mkNonCanonical (setCtEvLoc ev (setCtLocSpan ctl ct_ls))--mkKnWanted-  :: CtLoc-  -> CType-  -> TcPluginM Ct-mkKnWanted loc (CType ty) = do-  kc_clas <- tcLookupClass knownNatClassName-  let kn_pred = mkClassPred kc_clas [ty]-  wantedCtEv <- newWanted loc kn_pred-  let wanted' = mkNonCanonical' loc wantedCtEv-  return wanted'

@@ -1,862 +0,0 @@-{-|-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 NamedFieldPuns  #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections   #-}-{-# LANGUAGE ViewPatterns    #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.Normalise-  ( plugin )-where---- external-import Control.Arrow       (second)-import Control.Monad       ((<=<), forM)-#if !MIN_VERSION_ghc(8,4,1)-import Control.Monad       (replicateM)-#endif-import Control.Monad.Trans.Writer.Strict-import Data.Either         (partitionEithers, rights)-import Data.IORef-import Data.List           (intersect, partition, stripPrefix, find)-import Data.Maybe          (mapMaybe, catMaybes)-import Data.Set            (Set, empty, toList, notMember, fromList, union)-import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)-#if MIN_VERSION_ghc(9,2,0)-import GHC.TcPluginM.Extra (lookupModule, lookupName)-#endif-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(9,0,0)-import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals-  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (naturalTy)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#else-import GHC.Builtin.Types (typeNatKind)-import GHC.Builtin.Types.Literals (typeNatLeqTyCon)-#endif-import GHC.Core (Expr (..))-import GHC.Core.Class (className)-import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo)-import GHC.Core.Predicate-  (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,-   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)-import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))-import GHC.Core.TyCon (TyCon)-import GHC.Core.Type-  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Plugin-  (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO,-   newEvVar)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Tc.Plugin (tcLookupTyCon)-#endif-import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..))-import GHC.Tc.Types.Constraint-  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence,-   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,-   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr)-import GHC.Tc.Types.Evidence (EvTerm (..), evCast, evId)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Data.FastString (fsLit)-import GHC.Types.Name.Occurrence (mkTcOcc)-import GHC.Unit.Module (mkModuleName)-#endif-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-#else-#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  (hasKey, knownNatClassName)-import PrelNames  (eqTyConKey, heqTyConKey)-import TcEvidence (EvTerm (..))-#if MIN_VERSION_ghc(8,6,0)-import TcEvidence (evCast, evId)-#endif-#if !MIN_VERSION_ghc(8,4,0)-import TcPluginM  (zonkCt)-#endif-import TcPluginM  (TcPluginM, tcPluginTrace, tcPluginIO)-import Type-  (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe)-import TysWiredIn (typeNatKind)--import Coercion   (CoercionHole, Role (..), mkUnivCo)-import Class      (className)-import TcPluginM  (newCoercionHole, tcLookupClass, newEvVar)-import TcRnTypes  (TcPlugin (..), TcPluginResult(..))-import TyCoRep    (UnivCoProvenance (..))-import TcType     (isEqPred)-import TyCon      (TyCon)-import TyCoRep    (Type (..))-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,-                   typeNatSubTyCon)--import TcTypeNats (typeNatLeqTyCon)-import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)--#if MIN_VERSION_ghc(8,10,0)-import Constraint-  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,-   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,-   isWantedCt)-import Predicate-  (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,-   mkPrimEqPred, getClassPredTys_maybe)-import Type (typeKind)-#else-import TcRnTypes-  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence, ctEvLoc, ctEvPred,-   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan,-   isWantedCt)-import TcType (typeKind)-import Type-  (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkClassPred, mkPrimEqPred,-   getClassPredTys_maybe)-#if MIN_VERSION_ghc(8,4,0)-import Type (getEqPredTys)-#endif-#endif--#if MIN_VERSION_ghc(8,10,0)-import Constraint (ctEvExpr)-#elif MIN_VERSION_ghc(8,6,0)-import TcRnTypes  (ctEvExpr)-#else-import TcRnTypes  (ctEvTerm)-#endif--#if MIN_VERSION_ghc(8,2,0)-#if MIN_VERSION_ghc(8,10,0)-import Constraint (ShadowInfo (WDeriv))-#else-import TcRnTypes  (ShadowInfo (WDeriv))-#endif-#endif--#if MIN_VERSION_ghc(8,10,0)-import TcType (isEqPrimPred)-#endif-#endif---- internal-import GHC.TypeLits.Normalise.SOP-import GHC.TypeLits.Normalise.Unify--#if MIN_VERSION_ghc(9,2,0)-typeNatKind :: Type-typeNatKind = naturalTy-#endif--#if !MIN_VERSION_ghc(8,10,0)-isEqPrimPred :: PredType -> Bool-isEqPrimPred = isEqPred-#endif--isEqPredClass :: PredType -> Bool-isEqPredClass ty = case tyConAppTyCon_maybe ty of-  Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey-  _ -> False---- | To use the plugin, add------ @--- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}--- @------ To the header of your file.-plugin :: Plugin-plugin-  = defaultPlugin-  { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument-#if MIN_VERSION_ghc(8,6,0)-  , pluginRecompile = purePlugin-#endif-  }- where-  parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })-  parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })-  parseArgument _ = Nothing-  defaultOpts = Opts { negNumbers = False, depth = 5 }--data Opts = Opts { negNumbers :: Bool, depth :: Word }--normalisePlugin :: Opts -> TcPlugin-normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise"-  TcPlugin { tcPluginInit  = lookupExtraDefs-           , tcPluginSolve = decideEqualSOP opts-           , tcPluginStop  = const (return ())-           }-newtype OrigCt = OrigCt { runOrigCt :: Ct }--type ExtraDefs = (IORef (Set CType), TyCon)--lookupExtraDefs :: TcPluginM ExtraDefs-lookupExtraDefs = do-    ref <- tcPluginIO (newIORef empty)-#if !MIN_VERSION_ghc(9,2,0)-    return (ref, typeNatLeqTyCon)-#else-    md <- lookupModule myModule myPackage-    ordCond <- look md "OrdCond"-    return (ref, ordCond)-  where-    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)-    myModule  = mkModuleName "Data.Type.Ord"-    myPackage = fsLit "base"-#endif--decideEqualSOP-  :: Opts-  -> ExtraDefs-      -- ^ 1. Givens that is already generated.-      --   We have to generate new givens at most once;-      --   otherwise GHC will loop indefinitely.-      ---      ---      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond-      --      For older: TyCon of GHC.TypeLits.<=?-  -> [Ct]-  -> [Ct]-  -> [Ct]-  -> TcPluginM TcPluginResult---- Simplification phase: Derives /simplified/ givens;--- we can reduce given constraints like @Show (Foo (n + 2))@--- to its normal form @Show (Foo (2 + n))@, which is eventually--- useful in solving phase.------ This helps us to solve /indirect/ constraints;--- without this phase, we cannot derive, e.g.,--- @IsVector UVector (Fin (n + 1))@ from--- @Unbox (1 + n)@!-decideEqualSOP opts (gen'd,ordCond) givens _deriveds [] = do-    done <- tcPluginIO $ readIORef gen'd-#if MIN_VERSION_ghc(8,4,0)-    let simplGivens = flattenGivens givens-#else-    simplGivens <- mapM zonkCt givens-#endif-    let reds =-          filter (\(_,(_,_,v)) -> null v || negNumbers opts) $-          reduceGivens opts ordCond done simplGivens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds-    tcPluginIO $-      modifyIORef' gen'd $ union (fromList newlyDone)-    newGivens <- forM reds $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm-    return (TcPluginOk [] newGivens)---- Solving phase.--- Solves in/equalities on Nats and simplifiable constraints--- containing naturals.-decideEqualSOP opts (gen'd,ordCond) givens deriveds wanteds = do-    -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out-    let flat_wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds-#if MIN_VERSION_ghc(8,4,0)-    -- flattenGivens should actually be called unflattenGivens-    let simplGivens = givens ++ flattenGivens givens-        subst = fst $ unzip $ TcPluginM.mkSubst' givens-        unflattenWanted (oCt, ct) = (oCt, TcPluginM.substCt subst ct)-        unflat_wanteds0 = map unflattenWanted flat_wanteds0-#else-    let unflat_wanteds0 = flat_wanteds0-    simplGivens <- mapM zonkCt givens-#endif-    let unflat_wanteds1 = filter (isWanted . ctEvidence . snd) unflat_wanteds0-        -- only return solve deriveds when there are wanteds to solve-        unflat_wanteds2 = case unflat_wanteds1 of-                     [] -> []-                     w  -> w ++ (map (\a -> (OrigCt a,a)) deriveds)-        unit_wanteds = mapMaybe (toNatEquality ordCond) unflat_wanteds2-        nonEqs = filter (not . (\p -> isEqPred p || isEqPrimPred p) . ctEvPred . ctEvidence.snd)-                 $ filter (isWanted. ctEvidence.snd) unflat_wanteds0-    done <- tcPluginIO $ readIORef gen'd-    let redGs = reduceGivens opts ordCond done simplGivens-        newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs-    redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) ->-      mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm-    reducible_wanteds-      <- catMaybes <$>-            mapM-              (\(origCt, ct) -> fmap (runOrigCt origCt,) <$>-                  reduceNatConstr (simplGivens ++ redGivens) ct-              )-            nonEqs-    if null unit_wanteds && null reducible_wanteds-    then return $ TcPluginOk [] []-    else do-        -- Since reducible wanteds also can have some negation/subtraction-        -- subterms, we have to make sure appropriate inequalities to hold.-        -- Here, we generate such additional inequalities for reduction-        -- that is to be added to new [W]anteds.-        ineqForRedWants <- fmap concat $ forM redGs $ \(ct, (_,_, ws)) -> forM ws $-          fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct)-        tcPluginIO $-          modifyIORef' gen'd $ union (fromList newlyDone)-        let unit_givens = mapMaybe-                            (toNatEquality ordCond)-                            (map (\a -> (OrigCt a, a)) simplGivens)-        sr <- simplifyNats opts ordCond unit_givens unit_wanteds-        tcPluginTrace "normalised" (ppr sr)-        reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do-          wants <- evSubtPreds origCt $ subToPred opts ordCond ws-          return ((term, origCt), wDicts ++ wants)-        case sr of-          Simplified evs -> do-            let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs-                -- Only solve derived when we solved a wanted-                simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of-                            [] -> []-                            _  -> simpld-                (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds)-            return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants)-          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])--type NatEquality   = (Ct,CoreSOP,CoreSOP)-type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))--reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts ordCond done givens =-  let nonEqs =-        [ ct-        | ct <- givens-        , let ev = ctEvidence ct-              prd = ctEvPred ev-        , isGiven ev-        , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd-        ]-  in filter-      (\(_, (prd, _, _)) ->-        notMember (CType prd) done-      )-    $ mapMaybe-      (\ct -> (ct,) <$> tryReduceGiven opts ordCond givens ct)-      nonEqs--tryReduceGiven-  :: Opts -> TyCon -> [Ct] -> Ct-  -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts ordCond simplGivens ct = do-    let (mans, ws) =-          runWriter $ normaliseNatEverywhere $-          ctEvPred $ ctEvidence ct-        ws' = [ p-              | (p, _) <- subToPred opts ordCond ws-              , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens-              ]-    pred' <- mans-    return (pred', toReducedDict (ctEvidence ct) pred', ws')--fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left  (ct, _, _)) = ct-fromNatEquality (Right (ct, _))    = ct--reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct]))-reduceNatConstr givens ct =  do-  let pred0 = ctEvPred $ ctEvidence ct-      (mans, tests) = runWriter $ normaliseNatEverywhere pred0-  case mans of-    Nothing -> return Nothing-    Just pred' -> do-      case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of-        -- No existing evidence found-        Nothing -> case getClassPredTys_maybe pred' of-          -- Are we trying to solve a class instance?-          Just (cls,_) | className cls /= knownNatClassName -> do-            -- Create new evidence binding for normalized class constraint-            evVar <- newEvVar pred'-            -- Bind the evidence to a new wanted normalized class constraint-            let wDict = mkNonCanonical-                          (CtWanted pred' (EvVarDest evVar)-#if MIN_VERSION_ghc(8,2,0)-                          WDeriv-#endif-                          (ctLoc ct))-            -- Evidence for current wanted is simply the coerced binding for-            -- the new binding-                evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")-                         Representational-                         pred' pred0-#if MIN_VERSION_ghc(8,6,0)-                ev = evId evVar `evCast` evCo-#else-                ev = EvId evVar `EvCast` evCo-#endif-            -- Use newly created coerced wanted as evidence, and emit the-            -- normalized wanted as a new constraint to solve.-            return (Just (ev, tests, [wDict]))-          _ -> return Nothing-        -- Use existing evidence-        Just c  -> return (Just (toReducedDict (ctEvidence c) pred0, tests, []))--toReducedDict :: CtEvidence -> PredType -> EvTerm-toReducedDict ct pred' =-  let pred0 = ctEvPred ct-      evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")-              Representational-              pred0 pred'-#if MIN_VERSION_ghc(8,6,0)-      ev = ctEvExpr ct-             `evCast` evCo-#else-      ev = ctEvTerm ct `EvCast` evCo-#endif-  in ev--data SimplifyResult-  = Simplified [((EvTerm,Ct),[Ct])]-  | Impossible (Either NatEquality NatInEquality)--instance Outputable SimplifyResult where-  ppr (Simplified evs) = text "Simplified" $$ ppr evs-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq--simplifyNats-  :: Opts-  -- ^ Allow negated numbers (potentially unsound!)-  -> TyCon-  -- ^ For GHc 9.2: TyCon of Data.Type.Ord.OrdCond-  --   For older: TyCon of GHC.TypeLits.<=?-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Given constraints-  -> [(Either NatEquality NatInEquality,[(Type,Type)])]-  -- ^ Wanted constraints-  -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} ordCond eqsG eqsW = do-    let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG-        (varEqs,otherEqs) = partition isVarEqs eqsG1-        fancyGivens = concatMap (makeGivensSet otherEqs) varEqs-    case varEqs of-      [] -> do-        let eqs = otherEqs ++ eqsW-        tcPluginTrace "simplifyNats" (ppr eqs)-        simples [] [] [] [] eqs-      _  -> do-        tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")-                      (ppr varEqs)--        allSimplified <- forM fancyGivens $ \v -> do-          let eqs = v ++ eqsW-          tcPluginTrace "simplifyNats" (ppr eqs)-          simples [] [] [] [] eqs--        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)-  where-    simples :: [CoreUnify]-            -> [((EvTerm, Ct), [Ct])]-            -> [(CoreSOP,CoreSOP,Bool)]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> [(Either NatEquality NatInEquality,[(Type,Type)])]-            -> TcPluginM SimplifyResult-    simples _subst evs _leqsG _xs [] = return (Simplified evs)-    simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do-      let u' = substsSOP subst u-          v' = substsSOP subst v-      ur <- unifyNats ct u' v'-      tcPluginTrace "unifyNats result" (ppr ur)-      case ur of-        Win -> do-          evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts ordCond k)-          simples subst evs' leqsG [] (xs ++ eqs')-        Lose -> if null evs && null eqs'-                   then return (Impossible (fst eq))-                   else simples subst evs leqsG xs eqs'-        Draw [] -> simples subst evs [] (eq:xs) eqs'-        Draw subst' -> do-          evM <- evMagic ct empty (map unifyItemToPredType subst' ++-                                   subToPred opts ordCond k)-          let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG-                     | otherwise  = leqsG-          case evM of-            Nothing -> simples subst evs leqsG' xs eqs'-            Just ev ->-              simples (substsSubst subst' subst ++ subst')-                      (ev:evs) leqsG' [] (xs ++ eqs')-    simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do-      let u'    = substsSOP subst (subtractIneq u)-          x'    = substsSOP subst x-          y'    = substsSOP subst y-          uS    = (x',y',b)-          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG-                 | otherwise               = leqsG-          ineqs = concat [ leqsG-                         , map (substLeq subst) leqsG-                         , map snd (rights (map fst eqsG))-                         ]-      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))-      case runWriterT (isNatural u') of-        Just (True,knW)  -> do-          evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts ordCond k)-          simples subst evs' leqsG' xs eqs'--        Just (False,_) | null k -> return (Impossible (fst eq))-        _ -> do-          let solvedIneq = mapMaybe runWriterT-                 -- it is an inequality that can be instantly solved, such as-                 -- `1 <= x^y`-                 -- OR-                (instantSolveIneq depth u:-                instantSolveIneq depth uS:-                -- 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.-                -- OR-                map (solveIneq depth u) ineqs ++-                -- The above, but with valid substitutions applied to the wanted.-                map (solveIneq depth uS) ineqs)-              smallest = solvedInEqSmallestConstraint solvedIneq-          case smallest of-            (True,kW) -> do-              evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts ordCond k)-              simples subst evs' leqsG' xs eqs'-            _ -> simples subst evs leqsG (eq:xs) eqs'--    eqToLeq x y = [(x,y,True),(y,x,True)]-    substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)--    isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _) = True-    isVarEqs _ = False--    makeGivensSet otherEqs varEq-      = let (noMentionsV,mentionsV)   = partitionEithers-                                          (map (matchesVarEq varEq) otherEqs)-            (mentionsLHS,mentionsRHS) = partitionEithers mentionsV-            vS = swapVar varEq-            givensLHS = case mentionsLHS of-              [] -> []-              _  -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]-            givensRHS = case mentionsRHS of-              [] -> []-              _  -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]-        in  case mentionsV of-              [] -> [noMentionsV]-              _  -> givensLHS ++ givensRHS--    matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]),_) r = case r of-      (Left (_,S [P [V v3]],_),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Left (_,_,S [P [V v3]]),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(S [P [V v3]],_,_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      (Right (_,(_,S [P [V v3]],_)),_)-        | v1 == v3 -> Right (Left r)-        | v2 == v3 -> Right (Right r)-      _ -> Left r-    matchesVarEq _ _ = error "internal error"--    swapVar (Left (ct,S [P [V v1]], S [P [V v2]]),ps) =-      (Left (ct,S [P [V v2]], S [P [V v1]]),ps)-    swapVar _ = error "internal error"--    findFirstSimpliedWanted (Impossible e)   _  = Impossible e-    findFirstSimpliedWanted (Simplified evs) s2-      | any (isWantedCt . snd . fst) evs-      = Simplified evs-      | otherwise-      = s2---- 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 :: Opts -> TyCon -> [(Type, Type)] -> [(PredType, Kind)]-subToPred Opts{..} ordCond-  | negNumbers = const []-  | otherwise  = map (subtractionToPred ordCond)---- Extract the Nat equality constraints-toNatEquality :: TyCon -> (OrigCt, Ct) -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality ordCond (OrigCt oCt, ct) = case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2-      -> go t1 t2-    _ -> Nothing-  where-    go (TyConApp tc xs) (TyConApp tc' ys)-      | tc == tc'-      , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon-                                   ,typeNatMulTyCon,typeNatExpTyCon])-      = case filter (not . uncurry eqType) (zip xs ys) of-          [(x,y)]-            | isNatKind (typeKind x)-            , isNatKind (typeKind y)-            , let (x',k1) = runWriter (normaliseNat x)-            , let (y',k2) = runWriter (normaliseNat y)-            -> Just (Left (oCt, x', y'),k1 ++ k2)-          _ -> Nothing-#if MIN_VERSION_ghc(9,2,0)-      | tc == ordCond-      , [_,cmp,lt,eq,gt] <- xs-      , TyConApp tcCmpNat [x,y] <- cmp-      , tcCmpNat == typeNatCmpTyCon-      , TyConApp ltTc [] <- lt-      , ltTc == promotedTrueDataCon-      , TyConApp eqTc [] <- eq-      , eqTc == promotedTrueDataCon-      , TyConApp gtTc [] <- gt-      , gtTc == promotedFalseDataCon-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = case tc' of-         _ | tc' == promotedTrueDataCon-           -> Just (Right (oCt, (x', y', True)), ks)-         _ | tc' == promotedFalseDataCon-           -> Just (Right (oCt, (x', y', False)), ks)-         _ -> Nothing-#else-      | tc == ordCond-      , [x,y] <- xs-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      , let ks      = k1 ++ k2-      = case tc' of-         _ | tc' == promotedTrueDataCon-           -> Just (Right (oCt, (x', y', True)), ks)-         _ | tc' == promotedFalseDataCon-           -> Just (Right (oCt, (x', y', False)), ks)-         _ -> Nothing-#endif--    go x y-      | isNatKind (typeKind x)-      , isNatKind (typeKind y)-      , let (x',k1) = runWriter (normaliseNat x)-      , let (y',k2) = runWriter (normaliseNat y)-      = Just (Left (oCt,x',y'),k1 ++ k2)-      | otherwise-      = Nothing--    isNatKind :: Kind -> Bool-    isNatKind = (`eqType` typeNatKind)--unifyItemToPredType :: CoreUnify -> (PredType,Kind)-unifyItemToPredType ui =-    (mkPrimEqPred ty1 ty2,typeNatKind)-  where-    ty1 = case ui of-            SubstItem {..} -> mkTyVarTy siVar-            UnifyItem {..} -> reifySOP siLHS-    ty2 = case ui of-            SubstItem {..} -> reifySOP siSOP-            UnifyItem {..} -> reifySOP siRHS--evSubtPreds :: Ct -> [(PredType,Kind)] -> TcPluginM [Ct]-evSubtPreds ct preds = do-  let predTypes = map fst preds-#if MIN_VERSION_ghc(8,4,1)-  holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes-#else-  holes <- replicateM (length preds) newCoercionHole-#endif-  return (zipWith (unifyItemToCt (ctLoc ct)) predTypes holes)--evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))-evMagic ct knW preds = case classifyPredType $ ctEvPred $ ctEvidence ct of-  EqPred NomEq t1 t2 -> do-    holeWanteds <- evSubtPreds ct preds-    knWanted <- mapM (mkKnWanted ct) (toList knW)-    let newWant = knWanted ++ holeWanteds-        ctEv    = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2-#if MIN_VERSION_ghc(8,5,0)-    return (Just ((EvExpr (Coercion ctEv), ct),newWant))-#else-    return (Just ((EvCoercion ctEv, ct),newWant))-#endif-  _ -> return Nothing--mkNonCanonical' :: CtLoc -> CtEvidence -> Ct-mkNonCanonical' origCtl ev =-  let ct_ls   = ctLocSpan origCtl-      ctl     = ctEvLoc  ev-  in setCtLoc (mkNonCanonical ev) (setCtLocSpan ctl ct_ls)--mkKnWanted-  :: Ct-  -> CType-  -> TcPluginM Ct-mkKnWanted ct (CType ty) = do-  kc_clas <- tcLookupClass knownNatClassName-  let kn_pred = mkClassPred kc_clas [ty]-  wantedCtEv <- TcPluginM.newWanted (ctLoc ct) kn_pred-  let wanted' = mkNonCanonical' (ctLoc ct) wantedCtEv-  return wanted'--unifyItemToCt :: CtLoc-              -> PredType-              -> CoercionHole-              -> Ct-unifyItemToCt loc pred_type hole =-  mkNonCanonical-    (CtWanted-      pred_type-      (HoleDest hole)-#if MIN_VERSION_ghc(8,2,0)-      WDeriv-#endif-      loc)

@@ -0,0 +1,731 @@+{-|+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 DataKinds             #-}+{-# LANGUAGE ExplicitNamespaces    #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE NamedFieldPuns        #-}+{-# LANGUAGE RecordWildCards       #-}+{-# LANGUAGE TupleSections         #-}+{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+{-# OPTIONS_HADDOCK show-extensions #-}++module GHC.TypeLits.Normalise+  ( plugin )+where++-- base+import Control.Arrow+  ( second )+import Control.Monad+  ( (<=<) )+import Control.Monad.Trans.Writer.Strict+  ( WriterT(runWriterT), runWriter )+import Data.Either+  ( rights, partitionEithers )+import Data.List+  ( stripPrefix, find, partition )+import qualified Data.List.NonEmpty as NE+import Data.Maybe+  ( mapMaybe, catMaybes, fromMaybe )+import Data.Traversable+  ( for )+import Text.Read+  ( readMaybe )++-- containers+import Data.Set+  ( Set )+import qualified Data.Set as Set+  ( elems, empty )++-- ghc+import GHC.Builtin.Names+  ( knownNatClassName )+import GHC.Builtin.Types.Literals+  ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )++-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst+  ( TyConSubst, mkTyConSubst, splitTyConApp_upTo )+import GHC.Plugins+  ( Plugin(..), defaultPlugin, purePlugin )+import GHC.Utils.Outputable+  ( ($$), (<+>), text, vcat )++-- ghc-typelits-natnormalise+import GHC.TypeLits.Normalise.Compat+import GHC.TypeLits.Normalise.SOP+  ( SOP(S), Product(P), Symbol(V) )+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+  = defaultPlugin+  { tcPlugin = \ p -> do opts <- foldr id defaultOpts <$> traverse parseArgument p+                         return $ mkTcPlugin $ normalisePlugin opts+  , pluginRecompile = purePlugin+  }+ where+  parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True })+  parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth })+  parseArgument _ = Nothing+  defaultOpts = Opts { negNumbers = False, depth = 5 }++data Opts = Opts { negNumbers :: Bool, depth :: Word }++normalisePlugin :: Opts -> TcPlugin+normalisePlugin opts =+  TcPlugin { tcPluginInit    = lookupExtraDefs+           , tcPluginSolve   = decideEqualSOP opts+           , tcPluginRewrite = const emptyUFM+           , tcPluginStop    = const (return ())+           }++data ExtraDefs+  = ExtraDefs+    { tyCons :: LookedUpTyCons }++lookupExtraDefs :: TcPluginM Init ExtraDefs+lookupExtraDefs = do+  tcs <- lookupTyCons+  return $+    ExtraDefs+      { tyCons = tcs }++decideEqualSOP+  :: Opts+  -> ExtraDefs+      -- ^ 1. Givens that is already generated.+      --   We have to generate new givens at most once;+      --   otherwise GHC will loop indefinitely.+      --+      --+      --   2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond+      --      For older: TyCon of GHC.TypeLits.<=?+  -> [Ct]+  -> [Ct]+  -> TcPluginM Solve TcPluginSolveResult+-- Simplification phase: Derives /simplified/ givens;+-- we can reduce given constraints like @Show (Foo (n + 2))@+-- to its normal form @Show (Foo (2 + n))@, which is eventually+-- useful in solving phase.+--+-- This helps us to solve /indirect/ constraints;+-- without this phase, we cannot derive, e.g.,+-- @IsVector UVector (Fin (n + 1))@ from+-- @Unbox (1 + n)@!+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens [] =+   do+    let givensTyConSubst = mkTyConSubst givens+        reds =+          filter+            (\(_,(_,_,v)) -> null v || negNumbers opts) $+              reduceGivens opts tcs (mkTyConSubst givens) givens++    tcPluginTrace "decideEqualSOP Givens {" $+      vcat [ text "givens:" <+> ppr givens ]++    newGivens <- for reds $ \(origCt, (pred', evTerm, _)) ->+      mkNonCanonical <$> newGiven (ctLoc origCt) pred' evTerm+    -- Try to find contradictory Givens, to improve pattern match warnings.+    sr <- simplifyNats opts tcs [] $ concatMap (toNatEquality tcs givensTyConSubst) (givens ++ newGivens)+    case sr of+      Impossible eq -> do+        let contra = fromNatEquality eq+        tcPluginTrace "decideEqualSOP Givens (FAIL) }" $+          vcat [ text "givens:" <+> ppr givens+               , text "contra:" <+> ppr contra  ]+        return $ TcPluginContradiction [contra]+      Simplified {} -> do+        tcPluginTrace "decideEqualSOP Givens (OK) }" $+          vcat [ text "givens:" <+> ppr givens ]+        return $ TcPluginOk [] []++-- Solving phase.+-- Solves in/equalities on Nats and simplifiable constraints+-- containing naturals.+decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens wanteds0 = do+    deriveds <- askDeriveds+    let wanteds = if null wanteds0+                  then []+                  else wanteds0 ++ deriveds+        givensTyConSubst = mkTyConSubst givens+        unit_wanteds0 = concatMap (toNatEquality tcs givensTyConSubst) wanteds+        nonEqs = filter ( not+                        . (\p -> isEqPred p || isEqClassPred p)+                        . ctEvPred+                        . ctEvidence )+                 wanteds+    let newRedGs = reduceGivens opts tcs givensTyConSubst givens+    redGivens <- for newRedGs $ \(origCt, (pred', evExpr, _)) ->+      mkNonCanonical <$> newGiven (ctLoc origCt) pred' evExpr+    reducible_wanteds+      <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>+                                    reduceNatConstr givensTyConSubst (givens ++ redGivens) ct)+                            nonEqs++    tcPluginTrace "decideEqualSOP Wanteds {" $+       vcat [ text "givens:" <+> ppr givens+            , text "new reduced givens:" <+> ppr redGivens+            , text "newRedGs:" <+> ppr newRedGs+            , text $ replicate 80 '-'+            , text "wanteds:" <+> ppr wanteds+            , text "unit_wanteds:" <+> ppr unit_wanteds0+            , text "reducible_wanteds:" <+> ppr reducible_wanteds+            ]+    if null unit_wanteds0 && null reducible_wanteds+    then return $ TcPluginOk [] []+    else do+        -- Since reducible Wanteds also can have some negation/subtraction+        -- subterms, we have to make sure appropriate inequalities to hold.+        -- Here, we generate such additional inequalities for reduction+        -- that is to be added to new [W]anteds.+        ineqForRedWants <- fmap concat $ for newRedGs $ \(ct, (_,_, ws)) -> for ws $+          fmap mkNonCanonical . newWanted (ctLoc ct)+        let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) givens+            unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality tcs givensTyConSubst) ineqForRedWants+        sr <- simplifyNats opts tcs unit_givens unit_wanteds+        tcPluginTrace "normalised" (ppr sr)+        reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do+          wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws+          return ((term, origCt), wDicts ++ wants)+        case sr of+          Simplified evs -> do+            let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs+                -- Only solve a Derived when there are Wanteds in play+                simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of+                            [] -> []+                            _  -> simpld+                (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)++            tcPluginTrace "decideEqualSOP Wanteds }" $+               vcat [ text "givens:" <+> ppr givens+                    , text "new reduced givens:" <+> ppr redGivens+                    , text "newRedGs:" <+> ppr newRedGs+                    , text $ replicate 80 '-'+                    , text "wanteds:" <+> ppr wanteds+                    , text "ineqForRedWants:" <+> ppr ineqForRedWants+                    , text "unit_wanteds0:" <+> ppr (map (toNatEquality tcs givensTyConSubst) wanteds)+                    , text "unit_wanteds:" <+> ppr unit_wanteds+                    , text "reducible_wanteds:" <+> ppr reducible_wanteds+                    , text $ replicate 80 '='+                    , text "solved:" <+> ppr solved+                    , text "newWanteds:" <+> ppr newWanteds+                    ]++            return (TcPluginOk solved $ newWanteds)+          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])++type NatEquality   = (Ct,CoreSOP,CoreSOP)+type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))++reduceGivens :: Opts -> LookedUpTyCons+             -> TyConSubst+             -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]+reduceGivens opts tcs givensTyConSubst givens =+  let nonEqs =+        [ ct+        | ct <- givens+        , let ev = ctEvidence ct+              prd = ctEvPred ev+        , isGiven ev+        , not $ (\p -> isEqPred p || isEqClassPred p ) prd+        ]+  in mapMaybe+      (\ct -> (ct,) <$> tryReduceGiven opts tcs givensTyConSubst givens ct)+      nonEqs++tryReduceGiven+  :: Opts -> LookedUpTyCons+  -> TyConSubst+  -> [Ct] -> Ct+  -> Maybe (PredType, EvTerm, [PredType])+tryReduceGiven opts tcs givensTyConSubst simplGivens ct = do+    let (mans, ws) =+          runWriter $ normaliseNatEverywhere givensTyConSubst $+          ctEvPred $ ctEvidence ct+        ws' = [ p+              | p <- subToPred opts tcs ws+              , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens+              ]+        -- deps = unitDVarSet (ctEvId ct)+    (pred', deps) <- mans+    return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')++fromNatEquality :: Either NatEquality NatInEquality -> Ct+fromNatEquality (Left  (ct, _, _)) = ct+fromNatEquality (Right (ct, _))    = ct++reduceNatConstr :: TyConSubst -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))+reduceNatConstr givensTyConSubst givens ct = do+  let pred0 = ctEvPred $ ctEvidence ct+      (mans, tests) = runWriter $ normaliseNatEverywhere givensTyConSubst pred0++      -- Even if we didn't rewrite the Wanted,+      -- we may still be able to solve it from a (rewritten) Given.+      (pred', deps') = fromMaybe (pred0, []) mans+  case find ((`eqType` pred') . ctEvPred . ctEvidence) givens of+    -- No existing evidence found+    Nothing+      | ClassPred cls _ <- classifyPredType pred'+      , className cls /= knownNatClassName++      -- We actually did do some rewriting/normalisation.+      , Just {} <- mans+      -> do+          -- Create new evidence binding for normalized class constraint+          wtdDictCt <- mkNonCanonical <$> newWanted (ctLoc ct) pred'+          -- Evidence for current wanted is simply the coerced binding for+          -- the new binding+          let evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+                       Representational+                       deps'+                       pred' pred0+              ev = evCast (evId $ ctEvId wtdDictCt) evCo+          -- Use newly created coerced wanted as evidence, and emit the+          -- normalized wanted as a new constraint to solve.+          return (Just (EvExpr ev, tests, [wtdDictCt]))+      | otherwise+      -> return Nothing+    -- Use existing evidence+    Just c  -> return (Just (toReducedDict (ctEvidence c) pred0 deps', tests, []))++toReducedDict :: CtEvidence -> PredType -> [Coercion] -> EvTerm+toReducedDict ct pred' deps' =+  let pred0 = ctEvPred ct+      evCo = mkPluginUnivCo "ghc-typelits-natnormalise"+              Representational+              deps'+              pred0 pred'+      ev = evCast (ctEvExpr ct) evCo+  in EvExpr ev++data SimplifyResult+  = Simplified [((EvTerm,Ct),[Ct])]+  | Impossible (Either NatEquality NatInEquality)++instance Outputable SimplifyResult where+  ppr (Simplified evs) = text "Simplified" $$ ppr evs+  ppr (Impossible eq)  = text "Impossible" <+> ppr eq++type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion])++simplifyNats+  :: Opts+  -- ^ Allow negated numbers (potentially unsound!)+  -> LookedUpTyCons+  -> [NatCt]+  -- ^ Given constraints+  -> [NatCt]+  -- ^ Wanted constraints+  -> TcPluginM Solve SimplifyResult+simplifyNats opts@Opts {..} tcs eqsG eqsW = do+    let eqsG1 = map (\ (eq, _, deps) -> (eq, [] :: [(Type, Type)], deps)) eqsG+        (varEqs, otherEqs) = partition isVarEqs eqsG1+        fancyGivens = concatMap (makeGivensSet otherEqs) varEqs+    case varEqs of+      [] -> do+        let eqs = otherEqs ++ eqsW+        tcPluginTrace "simplifyNats" (ppr eqs)+        simples [] [] [] [] [] eqs+      _  -> do+        tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")+                      (ppr varEqs)++        allSimplified <- for fancyGivens $ \v -> do+          let eqs = v ++ eqsW+          tcPluginTrace "simplifyNats" (ppr eqs)+          simples [] [] [] [] [] eqs++        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)+  where+    simples :: [Coercion]+            -> [CoreUnify]+            -> [((EvTerm, Ct), [Ct])]+            -> [(CoreSOP,CoreSOP,Bool)]+            -> [NatCt]+            -> [NatCt]+            -> TcPluginM Solve SimplifyResult+    simples _ _subst evs _leqsG _xs [] = return (Simplified evs)+    simples deps subst evs leqsG xs (eq@(lr@(Left (ct,u,v)),k,deps2):eqs') = do+      let u' = substsSOP subst u+          v' = substsSOP subst v+      ur <- unifyNats ct u' v'+      tcPluginTrace "unifyNats result" (ppr ur)+      case ur of+        Win -> do+          evs' <- maybe evs (:evs) <$> evMagic tcs ct (deps ++ deps2) Set.empty (subToPred opts tcs k)+          simples deps subst evs' leqsG [] (xs ++ eqs')+        Lose -> if null evs && null eqs'+                   then return (Impossible lr)+                   else simples deps subst evs leqsG xs eqs'+        Draw [] -> simples deps subst evs [] (eq:xs) eqs'+        Draw subst' -> do+          evM <- evMagic tcs ct deps Set.empty (map unifyItemToPredType subst' +++                                                subToPred opts tcs k)++          tcPluginTrace "unifyNats: Draw (non-empty subst)" $+             vcat [ text "subst':" <+> ppr subst'+                  , text "evM:" <+> ppr evM ]++          let (leqsG1, deps1)+                | isGiven (ctEvidence ct) = ( eqToLeq u' v' ++ leqsG+                                            , ctEvCoercion (ctEvidence ct):deps)+                | otherwise               = (leqsG, deps)+          case evM of+            Nothing -> simples deps1 subst evs leqsG1 xs eqs'+            Just ev ->+              simples (ctEvCoercion (ctEvidence ct):deps ++ deps2)+                      (substsSubst subst' subst ++ subst')+                      (ev:evs) leqsG1 [] (xs ++ eqs')+    simples deps subst evs leqsG xs (eq@(lr@(Right (ct,u@(x,y,b))),k,deps2):eqs') = do+      let u'    = substsSOP subst (subtractIneq u)+          x'    = substsSOP subst x+          y'    = substsSOP subst y+          uS    = (x',y',b)+          leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG+                 | otherwise               = leqsG+          ineqs = concat [ leqsG+                         , map (substLeq subst) leqsG+                         , map snd (rights (map (\ (lr', _, _) -> lr') eqsG))+                         ]+      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs))+      case runWriterT (isNatural u') of+        Just (True,knW)  -> do+          evs' <- maybe evs (:evs) <$> evMagic tcs ct deps knW (subToPred opts tcs k)+          simples deps subst evs' leqsG' xs eqs'++        Just (False,_) | null k -> return (Impossible lr)+        _ -> do+          let solvedIneq = mapMaybe runWriterT+                 -- it is an inequality that can be instantly solved, such as+                 -- `1 <= x^y`+                 -- OR+                (instantSolveIneq depth u:+                instantSolveIneq depth uS:+                -- 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.+                -- OR+                map (solveIneq depth u) ineqs +++                -- The above, but with valid substitutions applied to the wanted.+                map (solveIneq depth uS) ineqs)+              smallest = solvedInEqSmallestConstraint solvedIneq+          case smallest of+            (True,kW) -> do+              let deps' = deps ++ deps2+              evs' <- maybe evs (:evs) <$> evMagic tcs ct deps' kW (subToPred opts tcs k)+              simples deps' subst evs' leqsG' xs eqs'+            _ -> simples deps subst evs leqsG (eq:xs) eqs'++    eqToLeq x y = [(x,y,True),(y,x,True)]+    substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b)++    isVarEqs (Left (_,S [P [V _]], S [P [V _]]), _, _) = True+    isVarEqs _ = False++    makeGivensSet :: [NatCt] -> NatCt -> [[NatCt]]+    makeGivensSet otherEqs varEq+      = let (noMentionsV,mentionsV)   = partitionEithers+                                          (map (matchesVarEq varEq) otherEqs)+            (mentionsLHS,mentionsRHS) = partitionEithers mentionsV+            vS = swapVar varEq+            givensLHS = case mentionsLHS of+              [] -> []+              _  -> [mentionsLHS ++ ((varEq:mentionsRHS) ++ noMentionsV)]+            givensRHS = case mentionsRHS of+              [] -> []+              _  -> [mentionsRHS ++ (vS:mentionsLHS ++ noMentionsV)]+        in  case mentionsV of+              [] -> [noMentionsV]+              _  -> givensLHS ++ givensRHS++    matchesVarEq :: NatCt+                 -> NatCt+                 -> Either NatCt (Either NatCt NatCt)+    matchesVarEq (Left (_, S [P [V v1]], S [P [V v2]]), _, _) r@(e, _, _) =+      case e of+        Left (_,S [P [V v3]],_)+          | v1 == v3 -> Right (Left r)+          | v2 == v3 -> Right (Right r)+        Left (_,_,S [P [V v3]])+          | v1 == v3 -> Right (Left r)+          | v2 == v3 -> Right (Right r)+        Right (_,(S [P [V v3]],_,_))+          | v1 == v3 -> Right (Left r)+          | v2 == v3 -> Right (Right r)+        Right (_,(_,S [P [V v3]],_))+          | v1 == v3 -> Right (Left r)+          | v2 == v3 -> Right (Right r)+        _ -> Left r+    matchesVarEq _ _ = error "internal error"++    swapVar (Left (ct,S [P [V v1]], S [P [V v2]]), ps, deps) =+      (Left (ct,S [P [V v2]], S [P [V v1]]), ps, deps)+    swapVar _ = error "internal error"++    findFirstSimpliedWanted (Impossible e)   _  = Impossible e+    findFirstSimpliedWanted (Simplified evs) s2+      | any (isWanted . ctEvidence . snd . fst) evs+      = Simplified evs+      | otherwise+      = s2++-- 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 :: Opts -> LookedUpTyCons -> [(Type, Type)] -> [PredType]+subToPred Opts{..} tcs+  | negNumbers = const []+  | otherwise  =+    -- Given 'a - b', require 'b <= a'.+    map (\ (a, b) -> mkLEqNat tcs b a)++-- | Extract all Nat equality and inequality constraints from another constraint.+toNatEquality :: LookedUpTyCons -> TyConSubst -> Ct -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]+toNatEquality tcs givensTyConSubst ct0+  | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0+  , let+      ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)+      ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)+      ks      = k1 ++ k2+  = case mbLTE of+      Nothing ->+        -- Equality constraint: x ~ y+        [(Left (ct0, x', y'), ks, cos0 ++ cos1 ++ cos2)]+      Just b ->+        -- Inequality constraint: (x <=? y) ~ b+        [(Right (ct0, (x', y', b)), ks, cos0 ++ cos1 ++ cos2)]+  | otherwise+  = case classifyPredType pred0 of+      EqPred NomEq t1 t2+        -> goNomEq t1 t2+      _ -> []+  where+    pred0 = ctPred ct0+    -- x ~ y+    goNomEq :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]+    goNomEq lhs rhs+      -- Recur into a TyCon application for TyCons that we **do not** rewrite,+      -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.+      | Just tcApps1 <- splitTyConApp_upTo givensTyConSubst lhs+      , Just tcApps2 <- splitTyConApp_upTo givensTyConSubst rhs+      , let tcAppsMap1 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps1+            tcAppsMap2 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps2+            tcAppPairs = intersectUniqMap_C (,) tcAppsMap1 tcAppsMap2+      , (tc, ((xs, cos1), (ys, cos2))):_ <- nonDetUniqMapToList tcAppPairs+      , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon]+      , let subs = filter (not . uncurry eqType) (zip xs ys)+      = (\ (eq, ws, deps) -> (eq, ws, cos1 ++ cos2 ++ deps)) <$>+          concatMap (uncurry rewrite) subs+      | otherwise+      = rewrite lhs rhs++    rewrite :: Type -> Type -> [(Either NatEquality NatInEquality, [(Type,Type)], [Coercion])]+    rewrite x y+      | isNatKind (typeKind x)+      , isNatKind (typeKind y)+      , let ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)+      , let ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)+      = [(Left (ct0,x',y'),k1 ++ k2, cos1 ++ cos2)]+      | otherwise+      = []++    isNatKind :: Kind -> Bool+    isNatKind = (`eqType` natKind)++unifyItemToPredType :: CoreUnify -> PredType+unifyItemToPredType ui = mkEqPredRole Nominal ty1 ty2+  where+    ty1 = case ui of+            SubstItem {..} -> mkTyVarTy siVar+            UnifyItem {..} -> reifySOP siLHS+    ty2 = case ui of+            SubstItem {..} -> reifySOP siSOP+            UnifyItem {..} -> reifySOP siRHS++evSubtPreds :: CtLoc -> [PredType] -> TcPluginM Solve [Ct]+evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)++evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM Solve (Maybe ((EvTerm, Ct), [Ct]))+evMagic tcs ct deps knW preds = do+  holeWanteds <- evSubtPreds (ctLoc ct) preds+  knWanted <- mapM (mkKnWanted (ctLoc ct)) (Set.elems knW)+  let newWant = knWanted ++ holeWanteds+  case classifyPredType $ ctEvPred $ ctEvidence ct of+    EqPred NomEq t1 t2 ->+      let ctEv = mkPluginUnivCo "ghc-typelits-natnormalise" Nominal deps t1 t2+      in return (Just ((EvExpr (Coercion ctEv), ct),newWant))+    IrredPred p ->+      let t1 = mkTyConApp (c0TyCon tcs) []+          co = mkPluginUnivCo "ghc-typelits-natnormalise" Representational deps t1 p+          dcApp = evDataConApp (c0DataCon tcs) [] []+       in return (Just ((EvExpr $ evCast dcApp co, ct),newWant))+    _ -> return Nothing++mkKnWanted+  :: CtLoc+  -> CType+  -> TcPluginM Solve Ct+mkKnWanted loc (CType ty) = do+  kc_clas <- tcLookupClass knownNatClassName+  let kn_pred = mkClassPred kc_clas [ty]+  wantedCtEv <- newWanted loc kn_pred+  return $ mkNonCanonical wantedCtEv

@@ -0,0 +1,381 @@++{-# 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)+      assertTyCon :: TyCon,+#endif+#if MIN_VERSION_ghc(9,1,0)+       -- | @<= :: k -> k -> Constraint@+      ordCondTyCon :: TyCon,+      leqTyCon :: TyCon,+#else+       -- | @<= :: Nat -> Nat -> Constraint@+      leqNatTyCon :: TyCon,+      -- | @<=? :: Nat -> Nat -> Constraint@+      leqQNatTyCon :: TyCon,+#endif+      cmpNatTyCon :: TyCon,+      c0TyCon   :: TyCon,+      c0DataCon :: DataCon+    }++lookupTyCons :: TcPluginM Init LookedUpTyCons+lookupTyCons = do+    cmpNatT <- lookupTHName ''GHC.TypeNats.CmpNat >>= tcLookupTyCon+#if MIN_VERSION_ghc(9,3,0)+    assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon+#endif+#if MIN_VERSION_ghc(9,1,0)+    leqT    <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon+    ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon+    return $+      LookedUpTyCons+        { leqTyCon     = leqT+        , ordCondTyCon = ordCond+#  if MIN_VERSION_ghc(9,3,0)+        , assertTyCon  = assertT+#  endif+        , cmpNatTyCon  = cmpNatT+        , c0TyCon      = cTupleTyCon 0+        , c0DataCon    = cTupleDataCon 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 tcs a 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.+  mkEqPredRole Nominal+    (mkTyConApp (leqTyCon tcs) [natKind, a, b])+    (mkTyConTy $ c0TyCon 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 givensTyConSubst =+  upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+  where+    go tc []+      | tc == promotedTrueDataCon+      = Just True+      | tc == promotedFalseDataCon+      = Just False+    go _ _ = Nothing++-- | Is this type 'LT', 'EQ' or 'GT'?+ordering_maybe :: TyConSubst -> Type -> Maybe (Ordering, [Coercion])+ordering_maybe givensTyConSubst =+  upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+  where+    go tc []+      | tc == promotedLTDataCon+      = Just LT+      | tc == promotedEQDataCon+      = Just EQ+      | tc == promotedGTDataCon+      = Just GT+    go _ _ = Nothing++#if MIN_VERSION_ghc(9,1,0)+cmpNat_maybe :: LookedUpTyCons -> TyConSubst -> Type -> Maybe ((Type, Type), [Coercion])+cmpNat_maybe tcs givensTyConSubst =+  upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+  where+    go tc [x,y]+      | tc == cmpNatTyCon tcs+      = Just (x,y)+    go _ _ = Nothing+#endif++-- | Is this type @() :: Constraint@?+unitCTuple_maybe :: TyConSubst -> PredType -> Maybe ((), [Coercion])+unitCTuple_maybe givensTyConSubst =+  upToGivens givensTyConSubst ( \ tc tys -> (, []) <$> go tc tys )+    where+      go tc []+        | isCTupleTyConName (tyConName tc)+        = Just ()+      go _ _ = 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 tcs givensTyConSubst ty0+  | EqPred NomEq x y <- classifyPredType ty0+  = if+      -- (b :: Bool) ~ y+      | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x+      -> second ( ++ cos1 ) <$> booleanRel b y+      -- x ~ (b :: Bool)+      | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst y+      -> second ( ++ cos1 ) <$> booleanRel b x+      | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst x+      -- (o :: Ordering) ~ y+      -> second ( ++ cos1 ) <$> orderingRel o y+      | Just ( o, cos1 ) <- ordering_maybe givensTyConSubst y+      -- x ~ (o :: Ordering)+      -> second ( ++ cos1 ) <$> orderingRel o x+      -- (() :: Constraint) ~ y+      | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst x+      -> second ( ++ cos1 ) <$> goTy y+      -- x ~ (() :: Constraint)+      | Just ( (), cos1 ) <- unitCTuple_maybe givensTyConSubst y+      -> second ( ++ cos1 ) <$> goTy x+      | otherwise+      -> Nothing+  | otherwise+  = goTy ty0+  where+    goTy :: PredType -> Maybe (Relation, [Coercion])+    goTy = upToGivens givensTyConSubst goTc++    goTc :: TyCon -> [Type] -> Maybe (Relation, [Coercion])+    goTc _tc _tys+#if MIN_VERSION_ghc(9,3,0)+      -- Look through 'Assert'.+      -- Case 4 in Note [Recognising Nat inequalities]+      | _tc == assertTyCon tcs+      , [ty, _] <- _tys+      = booleanRel True ty+#endif+      | otherwise+      = Nothing++    -- Recognise whether @(b :: Bool) ~ ty@ is an equality/inequality+    booleanRel :: Bool -> Type -> Maybe (Relation, [Coercion])+    booleanRel b = upToGivens givensTyConSubst (goBoolean b)++    goBoolean :: Bool -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+    goBoolean b tc tys+#if MIN_VERSION_ghc(9,1,0)+      -- OrdCond (CmpNat x y) lt eq gt ~ b+      -- Case 3 in Note [Recognising Nat inequalities]+      | tc == ordCondTyCon tcs+      , [_,cmp,ltTy,eqTy,gtTy] <- tys+      , Just (lt, cos1) <- boolean_maybe givensTyConSubst ltTy+      , Just (eq, cos2) <- boolean_maybe givensTyConSubst eqTy+      , Just (gt, cos3) <- boolean_maybe givensTyConSubst gtTy+      , Just ((x,y), cos4) <- cmpNat_maybe tcs givensTyConSubst cmp+      = ( , cos1 ++ cos2 ++ cos3 ++ cos4 ) <$>+        if -- (x <= y) ~ b+          | lt && eq && not gt+          -> Just ((x,y), Just b)+          -- (x < y) ~ b+          --   <=>+          -- (y <= x) ~ not b+          | lt && not eq && not gt+          -> Just ((y,x), Just $ not b)+          -- (x >= y) ~ b+          --  <=>+          -- (y <= x) ~ b+          | not lt && eq && gt+          -> Just ((y,x), Just b)+          -- (x > y) ~ b+          --   <=>+          -- (x <= y) ~ not b+          | not lt && not eq && gt+          -> Just ((x,y), Just $ not b)+          -- x ~ y+          |  ( b && not lt && eq && not gt )+          || ( not b && lt && not eq && gt )+          -> Just ((x,y), Nothing)+          | otherwise+          -> Nothing+#else+      -- (x <=? y) ~ b+      -- Case 2 in Note [Recognising Nat inequalities]+      | tc == leqQNatTyCon tcs+      , [x,y] <- tys+      = Just (((x,y), Just b), [])+#endif+      | otherwise+      = Nothing++    -- Recognise whether @(o :: Ordering) ~ ty@ is an equality/inequality+    orderingRel :: Ordering -> Type -> Maybe (Relation, [Coercion])+    orderingRel o = upToGivens givensTyConSubst (goOrdering o)++    goOrdering :: Ordering -> TyCon -> [Type] -> Maybe (Relation, [Coercion])+    goOrdering o tc tys+      -- CmpNat x y ~ o+      -- Case 1 in Note [Recognising Nat inequalities]+      | tc == cmpNatTyCon tcs+      , [x,y] <- tys+      = ( , [] ) <$>+        case o of+          EQ ->+            -- x ~ y+            Just ((x,y), Nothing)+          LT ->+            -- x < y  <=>  (y <= x) ~ False+            Just ((y,x), Just False)+          GT ->+            -- x > y  <=>  (x <= y) ~ False+            Just ((x,y), Just False)+      | otherwise+      = Nothing++upToGivens :: TyConSubst -> (TyCon -> [Type] -> Maybe (a, [Coercion])) -> Type -> Maybe (a, [Coercion])+upToGivens givensTyConSubst f ty =+  asum $ map ( \ (tc, tys, deps) -> second ( deps ++ ) <$> f tc tys ) $+    maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst 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

@@ -1,3 +1,4 @@+{-# LANGUAGE LambdaCase #-} {-| Copyright  :  (C) 2015-2016, University of Twente,                   2017     , QBayLogic B.V.@@ -74,8 +75,6 @@ @ -} -{-# LANGUAGE CPP #-}- module GHC.TypeLits.Normalise.SOP   ( -- * SOP types     Symbol (..)@@ -92,17 +91,18 @@   ) where --- External-import Data.Either (partitionEithers)-import Data.List   (sort)+-- base+import Data.Either+  ( partitionEithers )+import Data.List+  ( sort ) --- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Utils.Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)-#else-import Outputable (Outputable (..), (<+>), text, hcat, integer, punctuate)-#endif+-- ghc-tcplugin-api+import GHC.Utils.Outputable+  ( Outputable (..), (<+>), text, hcat, integer, punctuate ) +--------------------------------------------------------------------------------+ data Symbol v c   = I Integer                 -- ^ Integer constant   | C c                       -- ^ Non-integer constant@@ -160,7 +160,7 @@ -- 2^3          ==>  8 -- (k ^ i) ^ j  ==>  k ^ (i * j) -- @-reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c+reduceExp :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c reduceExp (E _                 (P [(I 0)])) = I 1        -- x^0 ==> 1 reduceExp (E (S [P [I 0]])     _          ) = I 0        -- 0^x ==> 0 reduceExp (E (S [P [(I i)]])   (P [(I j)]))@@ -189,7 +189,7 @@ -- x^4 * x  ==>  x^5 -- y*y      ==>  y^2 -- @-mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c+mergeS :: (Outputable v, Outputable c, Ord v, Ord c) => Symbol v c -> Symbol v c        -> Either (Symbol v c) (Symbol v c) mergeS (I i) (I j) = Left (I (i * j)) -- 8 * 7 ==> 56 mergeS (I 1) r     = Left r           -- 1 * x ==> x@@ -245,7 +245,8 @@ -- xy + 2xy   ==>  3xy -- xy + xy    ==>  2xy -- @-mergeP :: (Eq v, Eq c) => Product v c -> Product v c+mergeP :: (Eq v, Eq c, Outputable v, Outputable c)+       => Product v c -> Product v c        -> Either (Product v c) (Product v c) -- 2xy + 3xy ==> 5xy mergeP (P ((I i):is)) (P ((I j):js))@@ -272,7 +273,7 @@ -- (x + 2)^(2x)     ==>  (x^2 + 4xy + 4)^x -- (x + 2)^(y + 2)  ==>  4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2 -- @-normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+normaliseExp :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c -- b^1 ==> b normaliseExp b (S [P [I 1]]) = b @@ -296,7 +297,7 @@ normaliseExp b (S [e]) = S [P [reduceExp (E b e)]]  -- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2-normaliseExp b (S e) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) e)+normaliseExp b (S es) = foldr1 mergeSOPMul (map (normaliseExp b . S . (:[])) es)  zeroP :: Product v c -> Bool zeroP (P ((I 0):_)) = True@@ -311,7 +312,7 @@ -- * 'mergeS' -- * 'mergeP' -- * 'reduceExp'-simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c+simplifySOP :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c simplifySOP = repeatF go   where     go = mkNonEmpty@@ -329,12 +330,12 @@ {-# INLINEABLE simplifySOP #-}  -- | Merge two SOP terms by additions-mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPAdd :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPAdd (S sop1) (S sop2) = simplifySOP $ S (sop1 ++ sop2) {-# INLINEABLE mergeSOPAdd #-}  -- | Merge two SOP terms by multiplication-mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c+mergeSOPMul :: (Outputable v, Outputable c, Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c mergeSOPMul (S sop1) (S sop2)   = simplifySOP   . S

@@ -5,16 +5,15 @@ Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DataKinds                  #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash                  #-} {-# LANGUAGE RecordWildCards            #-}+{-# LANGUAGE TupleSections              #-} -{-# OPTIONS_GHC -fno-warn-unused-imports #-}-#if __GLASGOW_HASKELL__ < 801-#define nonDetCmpType cmpType-#endif +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ module GHC.TypeLits.Normalise.Unify   ( -- * 'Nat' expressions \<-\> 'SOP' terms     CType (..)@@ -38,7 +37,6 @@   , subtractIneq   , solveIneq   , ineqToSubst-  , subtractionToPred   , instantSolveIneq   , solvedInEqSmallestConstraint     -- * Properties@@ -46,82 +44,53 @@   ) where --- External-import Control.Arrow (first, second)+-- base+import Control.Arrow+  ( first, second ) import Control.Monad.Trans.Writer.Strict-import Data.Function (on)-import Data.List     ((\\), intersect, nub)-import Data.Maybe    (fromMaybe, mapMaybe, isJust)-import Data.Set      (Set)-import qualified Data.Set as Set+  ( Writer, WriterT(..), runWriter, tell )+import Data.Foldable+  ( asum )+import Data.Function+  ( on )+import Data.List+  ( (\\), intersect, nub )+import qualified Data.List.NonEmpty as NE+import Data.Maybe+  ( fromMaybe, mapMaybe, isJust )+import Data.Traversable+  ( for )+import GHC.Base+  ( (==#), isTrue# )+import GHC.Integer+  ( smallInteger )+import GHC.Integer.Logarithms+  ( integerLogBase# ) -import GHC.Base               (isTrue#,(==#))-import GHC.Integer            (smallInteger)-import GHC.Integer.Logarithms (integerLogBase#)+-- containers+import Data.Set+  ( Set )+import qualified Data.Set as Set --- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Types (boolTy, promotedTrueDataCon)+-- ghc import GHC.Builtin.Types.Literals-  (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (naturalTy, promotedFalseDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#else-import GHC.Builtin.Types (typeNatKind)-import GHC.Builtin.Types.Literals (typeNatLeqTyCon)-#endif-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)-import GHC.Core.TyCon (TyCon)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type-  (PredType, TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy, typeKind)-import GHC.Core.TyCo.Compare-  (eqType, nonDetCmpType)-#else-import GHC.Core.Type-  (PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind)-#endif-import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..))-import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)-import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)+  ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon+  ) import GHC.Types.Unique.Set-  (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet)-import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)-#else-import Outputable    (Outputable (..), (<+>), ($$), text)-import TcPluginM     (TcPluginM, tcPluginTrace)-import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,-                      typeNatSubTyCon, typeNatLeqTyCon)-import TyCon         (TyCon)-import Type          (TyVar,-                      coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,-                      nonDetCmpType, PredType, typeKind)-import TyCoRep       (Kind, Type (..), TyLit (..))-import TysWiredIn    (boolTy, promotedTrueDataCon, typeNatKind)-import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,-                      unitUniqSet)+  ( UniqSet+  , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet+  )+import GHC.Utils.Outputable+  ( ($$), (<+>), text ) -#if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct,  ctEvidence, ctEvId, ctEvPred, isGiven)-import Predicate  (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)-#else-import TcRnMonad  (Ct, ctEvidence, isGiven)-import TcRnTypes  (ctEvPred)-import Type       (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred)-#endif-#endif+-- ghc-tcplugin-api+import GHC.TcPlugin.API+import GHC.TcPlugin.API.TyConSubst (TyConSubst, splitTyConApp_upTo) --- Internal+-- ghc-typelits-natnormalise import GHC.TypeLits.Normalise.SOP --- Used for haddock-import GHC.TypeLits (Nat)--#if MIN_VERSION_ghc(9,2,0)-typeNatKind :: Type-typeNatKind = naturalTy-#endif+--------------------------------------------------------------------------------  newtype CType = CType { unCType :: Type }   deriving Outputable@@ -143,21 +112,45 @@ -- * literals -- * type variables -- * Applications of the arithmetic operators @(+,-,*,^)@-normaliseNat :: Type -> Writer [(Type,Type)] CoreSOP-normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1-normaliseNat (TyVarTy v)          = return (S [P [V v]])-normaliseNat (LitTy (NumTyLit i)) = return (S [P [I i]])-normaliseNat (TyConApp tc [x,y])-  | tc == typeNatAddTyCon = mergeSOPAdd <$> normaliseNat x <*> normaliseNat y-  | tc == typeNatSubTyCon = do-    tell [(x,y)]-    mergeSOPAdd <$> normaliseNat x-                <*> (mergeSOPMul (S [P [I (-1)]]) <$> normaliseNat y)-  | tc == typeNatMulTyCon = mergeSOPMul <$> normaliseNat x <*> normaliseNat y-  | tc == typeNatExpTyCon = normaliseExp <$> normaliseNat x <*> normaliseNat y-normaliseNat t = return (S [P [C (CType t)]])+normaliseNat :: TyConSubst -> Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])+normaliseNat givensTyConSubst ty+  | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty+  , (tc, xs, cos0) : _ <- NE.filter (( \ ( tc, _, _) -> tc `elem` knownTyCons)) tc_apps+  = second ( ++ cos0 ) <$> goTyConApp tc xs+  | Just i <- isNumLitTy ty+  = return (S [P [I i]], [])+  | Just v <- getTyVar_maybe ty+  = return (S [P [V v]], [])+  | otherwise+  = return (S [P [C (CType ty)]], [])+    where+      goTyConApp :: TyCon -> [Type] -> Writer [(Type,Type)] (CoreSOP, [Coercion])+      goTyConApp tc [x,y]+        | tc == typeNatAddTyCon =+            do (x', cos1) <- normaliseNat givensTyConSubst x+               (y', cos2) <- normaliseNat givensTyConSubst y+               return (mergeSOPAdd x' y', cos1 ++ cos2)+        | tc == typeNatSubTyCon = do+          (x', cos1) <- normaliseNat givensTyConSubst x+          (y', cos2) <- normaliseNat givensTyConSubst y+          tell [(reifySOP $ simplifySOP x', reifySOP $ simplifySOP y')]+          return (mergeSOPAdd x' (mergeSOPMul (S [P [I (-1)]]) y'), cos1 ++ cos2)+        | tc == typeNatMulTyCon =+          do (x', cos1) <- normaliseNat givensTyConSubst x+             (y', cos2) <- normaliseNat givensTyConSubst y+             return (mergeSOPMul x' y', cos1 ++ cos2)+        | tc == typeNatExpTyCon =+          do (x', cos1) <- normaliseNat givensTyConSubst x+             (y', cos2) <- normaliseNat givensTyConSubst y+             return (normaliseExp x' y', cos1 ++ cos2)+      goTyConApp tc xs =+        return (S [P [C (CType $ mkTyConApp tc xs)]], []) --- | Runs writer action. If the result /Nothing/ writer actions will be+knownTyCons :: [TyCon]+knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]+++-- | Runs writer action. If the result is /Nothing/, writer actions will be -- discarded. maybeRunWriter   :: Monoid a@@ -171,43 +164,50 @@ -- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce -- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is -- the same as input, returns @'Nothing'@.-normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)-normaliseNatEverywhere ty0-  | TyConApp tc _fields <- ty0-  , tc `elem` knownTyCons = do-    -- Normalize under current type constructor application. 'go' skips all-    -- known type constructors.-    ty1M <- maybeRunWriter (go ty0)-    let ty1 = fromMaybe ty0 ty1M--    -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'-    ty2 <- normaliseSimplifyNat ty1-    -- TODO: 'normaliseNat' could keep track whether it changed anything. That's-    -- TODO: probably cheaper than checking for equality here.-    pure (if ty2 `eqType` ty1 then ty1M else Just ty2)-  | otherwise = go ty0+normaliseNatEverywhere :: TyConSubst -> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+normaliseNatEverywhere givensTyConSubst ty0+  | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty0+  = fmap asum $ for tc_apps $ \ (tc, fields, cos1) ->+      if tc `elem` knownTyCons+      then do+        -- Normalize under current type constructor application. 'go' skips all+        -- known type constructors.+        ty1M <- maybeRunWriter (go tc fields)+        let (ty1, cos2) = fromMaybe (ty0, []) ty1M+        -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'+        (ty2, cos3) <- normaliseSimplifyNat givensTyConSubst ty1+        -- TODO: 'normaliseNat' could keep track whether it changed anything. That's+        -- TODO: probably cheaper than checking for equality here.+        pure (if ty2 `eqType` ty1 then second ((cos1 ++ cos2) ++) <$> ty1M else Just (ty2, cos1 ++ cos2 ++ cos3))+      else go tc fields+  | otherwise+  = pure Nothing  where-  knownTyCons :: [TyCon]-  knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]    -- Normalize given type, but ignore all top-level-  go :: Type -> Writer [(Type, Type)] (Maybe Type)-  go (TyConApp tc_ fields0_) = do+  go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))+  go tc_ fields0_ = do     fields1_ <- mapM (maybeRunWriter . cont) fields0_     if any isJust fields1_ then-      pure (Just (TyConApp tc_ (zipWith fromMaybe fields0_ fields1_)))+      let cos' = concat $ mapMaybe (fmap snd) fields1_+      in+         pure (Just (mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_), cos'))     else       pure Nothing    where-    cont = if tc_ `elem` knownTyCons then go else normaliseNatEverywhere-  go _ = pure Nothing+    cont ty'+      | tc_ `elem` knownTyCons+      , Just tc_apps' <- splitTyConApp_upTo givensTyConSubst ty'+      = asum <$> traverse ( \ (tc', flds', cos') -> fmap (second (cos' ++)) <$> go tc' flds') tc_apps'+      | otherwise+      = normaliseNatEverywhere givensTyConSubst ty' -normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type-normaliseSimplifyNat ty-  | typeKind ty `eqType` typeNatKind = do-      ty' <- normaliseNat ty-      return $ reifySOP $ simplifySOP ty'-  | otherwise = return ty+normaliseSimplifyNat :: TyConSubst -> Type -> Writer [(Type, Type)] (Type, [Coercion])+normaliseSimplifyNat givensTyConSubst ty+  | typeKind ty `eqType` natKind = do+      (ty', cos1) <- normaliseNat givensTyConSubst ty+      return $ (reifySOP $ simplifySOP ty', cos1)+  | otherwise = return (ty, [])  -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type@@ -257,11 +257,26 @@     -- at the "2 ^ -1" because of the negative exponent.     mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]                            -> [Either CoreSymbol (CoreSOP,[CoreProduct])]-    mergeExp (E s p)   []     = [Right (s,[p])]+    mergeExp (E (S [P [I 1]]) _) ys = ys+    mergeExp (E s p)             [] = [Right (s,[p])]+    mergeExp (E (S [P [I s1]]) p1) (y:ys)+      | Right ((S [P [I s2]]), p2s) <- y+      , let s = gcd s1 s2+            t1 = s1 `quot` s+            t2 = s2 `quot` s+      , s > 1+      -- Deal with e.g. "2 ^ -1 * 6 ^ x", where the bases differ.+      --+      --   (s * t1) ^ p1 * (s * t2) ^ (p2 + ...) * rest+      --     ===>+      --   s ^ (p1 + p2 + ...) * t1 ^ p1 * t2 ^ (p2 + ..) * rest+      = Right (S [P [I s]], (p1:p2s)) :+         mergeExp (E (S [P [I t1]]) p1)+           (Right ((S [P [I t2]]), p2s):ys)     mergeExp (E s1 p1) (y:ys)-      | Right (s2,p2) <- y+      | Right (s2,p2s) <- y       , s1 == s2-      = Right (s1,(p1:p2)) : ys+      = Right (s1,(p1:p2s)) : ys       | otherwise       = Right (s1,[p1]) : y : ys     mergeExp x ys = Left x : ys@@ -322,25 +337,6 @@ ineqToSubst _   = Nothing -subtractionToPred-  :: TyCon-  -> (Type,Type)-  -> (PredType, Kind)-subtractionToPred ordCond (x,y) =-#if MIN_VERSION_ghc(9,2,0)-  let cmpNat = mkTyConApp typeNatCmpTyCon [y,x]-      trueTc = mkTyConApp promotedTrueDataCon []-      falseTc = mkTyConApp promotedFalseDataCon []-      ordCmp = mkTyConApp ordCond-                [boolTy,cmpNat,trueTc,trueTc,falseTc]-      predTy = mkPrimEqPred ordCmp trueTc-   in (predTy,boolTy)-#else-  (mkPrimEqPred (mkTyConApp ordCond [y,x])-                (mkTyConApp promotedTrueDataCon [])-  ,boolTy)-#endif- -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints.@@ -359,18 +355,18 @@   ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS  -- | Apply a substitution to a single normalised 'SOP' term-substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c+substsSOP :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c substsSOP []                   u = u substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u) substsSOP ((UnifyItem {}):s)   u = substsSOP s u -substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c+substSOP :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c substSOP tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS -substProduct :: (Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c+substProduct :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c substProduct tv e = foldr1 mergeSOPMul . map (substSymbol tv e) . unP -substSymbol :: (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c+substSymbol :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c substSymbol _  _ s@(I _) = S [P [s]] substSymbol _  _ s@(C _) = S [P [s]] substSymbol tv e (V tv')@@ -379,7 +375,7 @@ substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p)  -- | Apply a substitution to a substitution-substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]+substsSubst :: (Outputable v, Outputable c, Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c] substsSubst s = map subt   where     subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}@@ -402,8 +398,8 @@ -- same, then we 'Win' if @u@ and @v@ are equal, and 'Lose' otherwise. -- -- If @u@ and @v@ do not have the same free variables, we result in a 'Draw',--- ware @u@ and @v@ are only equal when the returned 'CoreSubst' holds.-unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult+-- where @u@ and @v@ are only equal when the returned 'CoreSubst' holds.+unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM Solve UnifyResult unifyNats ct u v = do   tcPluginTrace "unifyNats" (ppr ct $$ ppr u $$ ppr v)   return (unifyNats' ct u v)@@ -422,7 +418,7 @@   where     -- A unifier is only a unifier if differs from the original constraint     diffFromConstraint (UnifyItem x y) = not (x == u && y == v)-    diffFromConstraint _               = True+    diffFromConstraint (SubstItem x y) = not (S [P [V x]] == u && y == v)  -- | Find unifiers for two SOP terms --@@ -461,32 +457,39 @@ unifiers ct u@(S [P [V x]]) v   = case classifyPredType $ ctEvPred $ ctEvidence ct of       EqPred NomEq t1 _-        | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [SubstItem x v]+        | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)+        -> [SubstItem x v]       _ -> [] unifiers ct u v@(S [P [V x]])   = case classifyPredType $ ctEvPred $ ctEvidence ct of       EqPred NomEq _ t2-        | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [SubstItem x u]+        | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)+        -> [SubstItem x u]       _ -> [] unifiers ct u@(S [P [C _]]) v   = case classifyPredType $ ctEvPred $ ctEvidence ct of       EqPred NomEq t1 t2-        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v]+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+        -> [UnifyItem u v]       _ -> [] unifiers ct u v@(S [P [C _]])   = case classifyPredType $ ctEvPred $ ctEvidence ct of       EqPred NomEq t1 t2-        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v]+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2+        -> [UnifyItem u v]       _ -> [] unifiers ct u v             = unifiers' ct u v  unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+unifiers' _ct (S [])        (S [])        = []+ unifiers' _ct (S [P [V x]]) (S [])        = [SubstItem x (S [P [I 0]])] unifiers' _ct (S [])        (S [P [V x]]) = [SubstItem x (S [P [I 0]])]  unifiers' _ct (S [P [V x]]) s             = [SubstItem x s] unifiers' _ct s             (S [P [V x]]) = [SubstItem x s] +unifiers' _ct (S [P [C {}]])   (S [P [C {}]])   = [] unifiers' _ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2] unifiers' _ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2] @@ -511,45 +514,41 @@ -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers, -- and `ceiling (logBase i j) == floor (logBase i j)` unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]])-  = case integerLogBase i j of-      Just k  -> unifiers' ct (S [p]) (S [P [I k]])-      Nothing -> []+  | Just k <- integerLogBase i j+  = unifiers' ct (S [p]) (S [P [I k]])  unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]])-  = case integerLogBase i j of-      Just k  -> unifiers' ct (S [p]) (S [P [I k]])-      Nothing -> []+  | Just k <- integerLogBase i j+  = unifiers' ct (S [p]) (S [P [I k]])  -- a^d * a^e ~ a^c ==> [c := d + e]-unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of-  Just (b:bs,ps) | all (== s1) (b:bs) ->-    unifiers' ct (S [p1]) (S ps)-  _ -> []+unifiers' ct (S [P [E s1 p1]]) (S [p2])+  | Just (b:bs,ps) <- collectBases p2+  , all (== s1) (b:bs)+  = unifiers' ct (S [p1]) (S ps) -unifiers' ct (S [p2]) (S [P [E s1 p1]]) = case collectBases p2 of-  Just (b:bs,ps) | all (== s1) (b:bs) ->-    unifiers' ct (S ps) (S [p1])-  _ -> []+unifiers' ct (S [p2]) (S [P [E s1 p1]])+  | Just (b:bs,ps) <- collectBases p2+  , all (== s1) (b:bs)+  = unifiers' ct (S ps) (S [p1])  -- (i * a) ~ j ==> [a := div j i] -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0-unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) =-  case safeDiv j i of-    Just k -> unifiers' ct (S [P ps]) (S [P [I k]])-    _      -> []+unifiers' ct (S [P ((I i):ps)]) (S [P [I j]])+  | Just k <- safeDiv j i+  = unifiers' ct (S [P ps]) (S [P [I k]]) -unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) =-  case safeDiv j i of-    Just k -> unifiers' ct (S [P ps]) (S [P [I k]])-    _      -> []+unifiers' ct (S [P [I j]]) (S [P ((I i):ps)])+  | Just k <- safeDiv j i+  = unifiers' ct (S [P ps]) (S [P [I k]])  -- (2*a) ~ (2*b) ==> [a := b] -- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) --     | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2]) --     | otherwise = [] unifiers' ct (S [P ps1]) (S [P ps2])-    | null psx  = []-    | otherwise = unifiers' ct (S [P ps1'']) (S [P ps2''])+  | not $ null psx+  = unifiers' ct (S [P ps1'']) (S [P ps2''])   where     ps1'  = ps1 \\ psx     ps2'  = ps2 \\ psx@@ -561,28 +560,32 @@  -- (2 + a) ~ 5 ==> [a := 3] unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))-    | i < j     = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))-    | i > j     = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)+  = case compare i j of+       EQ -> unifiers' ct (S ps1) (S ps2)+       LT -> unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))+       GT -> unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)  -- (a + c) ~ (b + c) ==> [a := b]-unifiers' ct s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of-  Just (s1',s2',_)-    | s1' /= s1 || s2' /= s1-    , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))-    , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))-    -> unifiers' ct s1' s2'-  _ | null psx-    , length ps1 == length ps2-    -> case nub (concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)) of-        []                             -> unifiers'' ct (S ps1) (S ps2)-        [k] | length ps1 == length ps2 -> [k]-        _                              -> []-    | null psx-    , isGiven (ctEvidence ct)-    -> unifiers'' ct (S ps1) (S ps2)-    | null psx-    -> []-  _ -> unifiers' ct (S ps1'') (S ps2'')+unifiers' ct s1@(S ps1) s2@(S ps2)+  | Just (s1',s2',_) <- sopToIneq k1+  , s1' /= s1 || s2' /= s2+  , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))+  , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))+  = unifiers' ct s1' s2'+  | null psx+  , length ps1 == length ps2+  , length ps1 > 1+  , let unifs = nub $ concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)+  , length unifs <= 1+  = case unifs of+        []  -> unifiers'' ct (S ps1) (S ps2)+        [k] -> [k]+        _   -> error "impossible"+  | null psx+  , isGiven (ctEvidence ct)+  = unifiers'' ct (S ps1) (S ps2)+  | not $ null psx+  = unifiers' ct (S ps1'') (S ps2'')   where     k1 = subtractIneq (s1,s2,True)     ps1'  = ps1 \\ psx@@ -592,6 +595,8 @@     ps2'' | null ps2' = [P [I 0]]           | otherwise = ps2'     psx = intersect ps1 ps2++unifiers' _ s1 s2 = [UnifyItem s1 s2]  unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2

@@ -20,13 +20,16 @@  import Data.Proxy import GHC.TypeLits-#if __GLASGOW_HASKELL__ >= 904+#if __GLASGOW_HASKELL__ >= 903 import GHC.Types #endif  import GHC.IO.Encoding            (getLocaleEncoding, textEncodingName, utf8) import Language.Haskell.TH        (litE, stringL) import Language.Haskell.TH.Syntax (runIO)+#if __GLASGOW_HASKELL__ >= 901+import qualified Data.Type.Ord+#endif  #if __GLASGOW_HASKELL__ >= 901 import qualified Data.Type.Ord@@ -90,11 +93,11 @@ testProxy4Errors = #if __GLASGOW_HASKELL__ >= 900   ["Expected: Proxy 2 -> ()"-  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"+  ,"  Actual: Proxy ((2 * 0) + 4) -> ()"   ] #else   ["Expected type: Proxy 2 -> ()"-  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+  ,"Actual type: Proxy ((2 * 0) + 4) -> ()"   ] #endif @@ -104,11 +107,11 @@ testProxy5Errors = #if __GLASGOW_HASKELL__ >= 900   ["Expected: Proxy 7 -> ()"-  ,"  Actual: Proxy ((2 * y1) + 4) -> ()"+  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"   ] #else   ["Expected type: Proxy 7 -> ()"-  ,"Actual type: Proxy ((2 * y1) + 4) -> ()"+  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"   ] #endif 

@@ -33,6 +33,10 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P +#if MIN_VERSION_base(4,16,0)+import Data.Type.Ord+#endif+ import Data.Kind (Type) import Data.List (isInfixOf) import Data.Proxy@@ -506,7 +510,7 @@ oneLtPowSubst = go   where     go :: 1 <= b => Proxy a -> Proxy a-    go = id +    go = id  main :: IO () main = defaultMain tests@@ -709,3 +713,37 @@   touchVector = WFV . touchVector . unWrap instance FakeUnbox (n + 1) => IsMVector WrapFakeMVector n where   touchMVector = MWFV . touchMVector . unWrapM++#if MIN_VERSION_base(4,16,0)+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/70+libFunc :: forall (i :: Nat) d. i < d => Proxy i -> Proxy d -> ()+libFunc _ _ = ()+useFunc :: forall (d :: Nat). Proxy d -> ()+useFunc _ = libFunc (Proxy @0) (Proxy @(d+1))+#endif++-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71+t1 :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> ()+t1 _ = ()+t2 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> ()+t2 px = t1 px++++type family TF (a :: Nat) (b :: Nat) :: Nat++proxyEq5+  :: forall a b+   . KnownNat (TF (a * 3) b * 3)+  => Proxy a+  -> Proxy b+  -> Proxy (3 * TF (3 * a) b)+proxyEq5 = theProxy+ where+  theProxy+    :: forall a b+     . KnownNat (TF (2 * a + a) b + (2 * TF (a + 2 * a) b))+    => Proxy a+    -> Proxy b+    -> Proxy (3 * TF (3 * a) b)+  theProxy _ _ = Proxy