ghc-typelits-extra 0.4 → 0.4.1

raw patch · 7 files changed

+257/−130 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• ghc-typelits-extra.cabal +1/−1
• src/GHC/TypeLits/Extra/Solver.hs +78/−49
• src/GHC/TypeLits/Extra/Solver/Operations.hs +62/−42
• src/GHC/TypeLits/Extra/Solver/Unify.hs +57/−38
• tests/ErrorTests.hs +8/−0
• tests/Main.hs +48/−0

@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.4.1 *November 10 2020*+* Reduce `n <=? Max (n + p) p` to `True`+ # 0.4 *March 9 2020* * `Max` short-circuits on zero, but is stuckness preserving. i.e. `Max (0-1) 0` reduces to `(0-1)` * Reduce inside arithmetic equations. e.g. `1 + a ~ Max 0 a + CLog 2 2`

@@ -1,5 +1,5 @@ name:                ghc-typelits-extra-version:             0.4+version:             0.4.1 synopsis:            Additional type-level operations on GHC.TypeLits.Nat description:   Additional type-level operations on @GHC.TypeLits.Nat@:

@@ -24,10 +24,9 @@  -- external import Control.Monad.Trans.Maybe (MaybeT (..))-import Data.Either               (lefts) import Data.Maybe                (catMaybes)-import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,-                                  tracePlugin)+import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName+                                 ,tracePlugin, newWanted)  -- GHC API import FastString (fsLit)@@ -38,10 +37,11 @@ #if MIN_VERSION_ghc(8,6,0) import Plugins    (purePlugin) #endif+import PrelNames  (eqPrimTyConKey, hasKey) import TcEvidence (EvTerm) import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace) import TcRnTypes  (TcPlugin(..), TcPluginResult (..))-import Type       (Kind, eqType)+import Type       (Kind, eqType, mkTyConApp, splitTyConApp_maybe) import TyCoRep    (Type (..)) import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon) import TcTypeNats (typeNatLeqTyCon)@@ -54,11 +54,11 @@ #endif  #if MIN_VERSION_ghc(8,10,0)-import Constraint (Ct, ctEvidence, ctEvPred, isWantedCt)+import Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) import Predicate  (EqRel (NomEq), Pred (EqPred), classifyPredType) import Type       (typeKind) #else-import TcRnTypes  (Ct, ctEvidence, ctEvPred, isWantedCt)+import TcRnTypes  (Ct, CtEvidence, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) import TcType     (typeKind) import Type       (EqRel (NomEq), PredTree (EqPred), classifyPredType) #endif@@ -114,100 +114,129 @@ decideEqualSOP defs givens  _deriveds wanteds = do   -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out   let wanteds' = filter isWantedCt wanteds-  unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'+  unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds'   case unit_wanteds of     [] -> return (TcPluginOk [] [])     _  -> do #if MIN_VERSION_ghc(8,4,0)-      unit_givens <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) (givens ++ flattenGivens givens)+      unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) (givens ++ flattenGivens givens) #else-      unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens+      unit_givens <- catMaybes <$> mapM ((runMaybeT . toSolverConstraint defs) <=< zonkCt) givens #endif-      sr <- simplifyExtra (unit_givens ++ unit_wanteds)+      sr <- simplifyExtra defs (unit_givens ++ unit_wanteds)       tcPluginTrace "normalised" (ppr sr)       case sr of-        Simplified evs -> return (TcPluginOk (filter (isWantedCt . snd) evs) [])-        Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq])+        Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new)+        Impossible eq  -> return (TcPluginContradiction [fromSolverConstraint eq]) -type NatEquality   = (Ct,ExtraOp,ExtraOp)-type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)+data SolverConstraint+   = NatEquality Ct ExtraOp ExtraOp Normalised+   | NatInequality Ct ExtraOp ExtraOp Bool Normalised +instance Outputable SolverConstraint where+  ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm+  ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm+ data SimplifyResult-  = Simplified [(EvTerm,Ct)]-  | Impossible (Either NatEquality NatInEquality)+  = Simplified [(EvTerm,Ct)] [Ct]+  | Impossible SolverConstraint  instance Outputable SimplifyResult where-  ppr (Simplified evs) = text "Simplified" $$ ppr evs-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq+  ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new+  ppr (Impossible sct)  = text "Impossible" <+> ppr sct -simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult-simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs+simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult+simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs   where-    simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult-    simples evs [] = return (Simplified (catMaybes evs))-    simples evs (eq@(Left (ct,u,v)):eqs') = do+    simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult+    simples evs news [] = return (Simplified (catMaybes evs) news)+    simples evs news (eq@(NatEquality ct u v norm):eqs') = do       ur <- unifyExtra ct u v       tcPluginTrace "unifyExtra result" (ppr ur)       case ur of-        Win  -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'-        Lose -> if null evs && null eqs'-                   then return  (Impossible eq)-                   else simples evs eqs'-        Draw -> simples evs eqs'-    simples evs (eq@(Right (ct,u,v,b)):eqs') = do+        Win                          -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'+        Lose | null evs && null eqs' -> return (Impossible eq)+        _ | norm == Normalised && isWantedCt ct -> do+          newCt <- createWantedFromNormalised defs eq+          simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'+        Lose -> simples evs news eqs'+        Draw -> simples evs news eqs'+    simples evs news (eq@(NatInequality ct u v b norm):eqs') = do       tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))       case (u,v) of         (I i,I j)-          | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+          | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'           | otherwise     -> return  (Impossible eq)         (p, Max x y)-          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs'          -- transform:  q ~ Max x y => (p <=? q ~ True)         -- to:         (p <=? Max x y) ~ True         -- and try to solve that along with the rest of the eqs'         (p, q@(V _))           | b -> case findMax q eqs of-                   Just m  -> simples evs ((Right (ct,p,m,b)):eqs')-                   Nothing -> simples evs eqs'-        _ -> simples evs eqs'+                   Just m  -> simples evs news (NatInequality ct p m b norm:eqs')+                   Nothing -> simples evs news eqs'+        _ | norm == Normalised && isWantedCt ct -> do+          newCt <- createWantedFromNormalised defs eq+          simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs'+        _ -> simples evs news eqs'      -- look for given constraint with the form: c ~ Max x y-    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp-    findMax c = go . lefts+    findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp+    findMax c = go       where         go [] = Nothing-        go ((ct, a,b@(Max _ _)) :_)+        go ((NatEquality ct a b@(Max _ _) _) :_)           | c == a && not (isWantedCt ct)             = Just b-        go ((ct, a@(Max _ _),b) :_)+        go ((NatEquality ct a@(Max _ _) b _) :_)           | c == b && not (isWantedCt ct)             = Just a         go (_:rest) = go rest   -- Extract the Nat equality constraints-toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)-toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint+toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq t1 t2       | isNatKind (typeKind t1) || isNatKind (typeKind t2)-      -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)+      -> do+         (t1', n1) <- normaliseNat defs t1+         (t2', n2) <- normaliseNat defs t2+         pure (NatEquality ct t1' t2' (mergeNormalised n1 n2))       | TyConApp tc [x,y] <- t1       , tc == typeNatLeqTyCon       , TyConApp tc' [] <- t2-      -> if tc' == promotedTrueDataCon-            then Right <$> ((ct,,,True) <$> normaliseNat defs x <*> normaliseNat defs y)-            else if tc' == promotedFalseDataCon-                 then Right <$> ((ct,,,False) <$> normaliseNat defs x <*> normaliseNat defs y)-                 else fail "Nothing"+      -> do+          (x', n1) <- normaliseNat defs x+          (y', n2) <- normaliseNat defs y+          let res | tc' == promotedTrueDataCon  = pure (NatInequality ct x' y' True  (mergeNormalised n1 n2))+                  | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2))+                  | otherwise                   = fail "Nothing"+          res     _ -> fail "Nothing"   where     isNatKind :: Kind -> Bool     isNatKind = (`eqType` typeNatKind) -fromNatEquality :: Either NatEquality NatInEquality -> Ct-fromNatEquality (Left (ct, _, _))  = ct-fromNatEquality (Right (ct,_,_,_)) = ct+createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct+createWantedFromNormalised defs sct = do+  let extractCtSides (NatEquality ct t1 t2 _)   = (ct, reifyEOP defs t1, reifyEOP defs t2)+      extractCtSides (NatInequality ct x y b _) = let tc = if b then promotedTrueDataCon else promotedFalseDataCon+                                                      t1 = TyConApp typeNatLeqTyCon [reifyEOP defs x, reifyEOP defs y]+                                                      t2 = TyConApp tc []+                                                    in (ct, t1, t2)+  let (ct, t1, t2) = extractCtSides sct+  newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of+    Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])+    _ -> fail "Nothing"+  ev <- newWanted (ctLoc ct) newPredTy+  return (ct { cc_ev = ev })++fromSolverConstraint :: SolverConstraint -> Ct+fromSolverConstraint (NatEquality ct _ _ _)  = ct+fromSolverConstraint (NatInequality ct _ _ _ _) = ct  lookupExtraDefs :: TcPluginM ExtraDefs lookupExtraDefs = do

@@ -11,6 +11,9 @@ module GHC.TypeLits.Extra.Solver.Operations   ( ExtraOp (..)   , ExtraDefs (..)+  , Normalised (..)+  , NormaliseResult+  , mergeNormalised   , reifyEOP   , mergeMax   , mergeMin@@ -42,6 +45,23 @@ import TyCon      (TyCon) import Type       (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) +-- | Indicates whether normalisation has occured+data Normalised = Normalised | Untouched+  deriving Eq++instance Outputable Normalised where+  ppr Normalised = text "Normalised"+  ppr Untouched  = text "Untouched"++mergeNormalised :: Normalised -> Normalised -> Normalised+mergeNormalised Normalised _ = Normalised+mergeNormalised _ Normalised = Normalised+mergeNormalised _ _          = Untouched++-- | A normalise result contains the ExtraOp and a flag that indicates whether any expression+-- | was normalised within the ExtraOp.+type NormaliseResult = (ExtraOp, Normalised)+ data ExtraOp   = I    Integer   | V    TyVar@@ -110,80 +130,80 @@ reifyEOP defs (Exp x y)  = mkTyConApp typeNatExpTyCon  [reifyEOP defs x                                                        ,reifyEOP defs y] -mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp-mergeMax _ (I 0) y = y-mergeMax _ x (I 0) = x+mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult+mergeMax _ (I 0) y = (y, Normalised)+mergeMax _ x (I 0) = (x, Normalised) mergeMax defs x y =   let x' = reifyEOP defs x       y' = reifyEOP defs y       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)   in  case runWriterT (isNatural z) of-        Just (True , cs) | Set.null cs -> y-        Just (False, cs) | Set.null cs -> x+        Just (True , cs) | Set.null cs -> (y, Normalised)+        Just (False, cs) | Set.null cs -> (x, Normalised) #else   in  case isNatural z of-        Just True  -> y-        Just False -> x+        Just True  -> (y, Normalised)+        Just False -> (x, Normalised) #endif-        _ -> Max x y+        _ -> (Max x y, Untouched) -mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp+mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult mergeMin defs x y =   let x' = reifyEOP defs x       y' = reifyEOP defs y       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)   in  case runWriterT (isNatural z) of-        Just (True, cs) | Set.null cs -> x-        Just (False,cs) | Set.null cs -> y+        Just (True, cs) | Set.null cs -> (x, Normalised)+        Just (False,cs) | Set.null cs -> (y, Normalised) #else   in  case isNatural z of-        Just True  -> x-        Just False -> y+        Just True  -> (x, Normalised)+        Just False -> (y, Normalised) #endif-        _ -> Min x y+        _ -> (Min x y, Untouched) -mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeDiv _     (I 0)      = Nothing-mergeDiv (I i) (I j)      = Just (I (div i j))-mergeDiv x y              = Just (Div x y)+mergeDiv (I i) (I j)      = Just (I (div i j), Normalised)+mergeDiv x y              = Just (Div x y, Untouched) -mergeMod :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeMod _     (I 0)      = Nothing-mergeMod (I i) (I j)      = Just (I (mod i j))-mergeMod x y              = Just (Mod x y)+mergeMod (I i) (I j)      = Just (I (mod i j), Normalised)+mergeMod x y              = Just (Mod x y, Untouched) -mergeFLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeFLog (I i) _         | i < 2  = Nothing-mergeFLog i     (Exp j k) | i == j = Just k-mergeFLog (I i) (I j)              = I <$> flogBase i j-mergeFLog x     y                  = Just (FLog x y)+mergeFLog i     (Exp j k) | i == j = Just (k, Normalised)+mergeFLog (I i) (I j)              = fmap (\r -> (I r, Normalised)) (flogBase i j)+mergeFLog x     y                  = Just (FLog x y, Untouched) -mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeCLog (I i) _         | i < 2  = Nothing-mergeCLog i     (Exp j k) | i == j = Just k-mergeCLog (I i) (I j)              = I <$> clogBase i j-mergeCLog x     y                  = Just (CLog x y)+mergeCLog i     (Exp j k) | i == j = Just (k, Normalised)+mergeCLog (I i) (I j)              = fmap (\r -> (I r, Normalised)) (clogBase i j)+mergeCLog x     y                  = Just (CLog x y, Untouched) -mergeLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeLog (I i) _          | i < 2   = Nothing-mergeLog b     (Exp b' y) | b == b' = Just y-mergeLog (I i) (I j)                = I <$> exactLogBase i j-mergeLog x     y                    = Just (Log x y)+mergeLog b     (Exp b' y) | b == b' = Just (y, Normalised)+mergeLog (I i) (I j)                = fmap (\r -> (I r, Normalised)) (exactLogBase i j)+mergeLog x     y                    = Just (Log x y, Untouched) -mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp-mergeGCD (I i) (I j) = I (gcd i j)-mergeGCD x     y     = GCD x y+mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult+mergeGCD (I i) (I j) = (I (gcd i j), Normalised)+mergeGCD x     y     = (GCD x y, Untouched) -mergeLCM :: ExtraOp -> ExtraOp -> ExtraOp-mergeLCM (I i) (I j) = I (lcm i j)-mergeLCM x     y     = LCM x y+mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult+mergeLCM (I i) (I j) = (I (lcm i j), Normalised)+mergeLCM x     y     = (LCM x y, Untouched) -mergeExp :: ExtraOp -> ExtraOp -> ExtraOp-mergeExp (I i) (I j)                = I (i^j)-mergeExp b     (Log b' y) | b == b' = y-mergeExp x     y                    = Exp x y+mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult+mergeExp (I i) (I j)                = (I (i^j), Normalised)+mergeExp b     (Log b' y) | b == b' = (y, Normalised)+mergeExp x     y                    = (Exp x y, Untouched)  -- | \x y -> logBase x y, x > 1 && y > 0 flogBase :: Integer -> Integer -> Maybe Integer

@@ -10,6 +10,7 @@ module GHC.TypeLits.Extra.Solver.Unify   ( ExtraDefs (..)   , UnifyResult (..)+  , NormaliseResult   , normaliseNat   , unifyExtra   )@@ -18,14 +19,13 @@ -- external import Control.Monad.Trans.Class    (lift) import Control.Monad.Trans.Maybe    (MaybeT (..))-import Control.Monad.Trans.Writer.Strict (runWriter)+import Data.Maybe                   (catMaybes) import Data.Function                (on) import GHC.TypeLits.Normalise.Unify (CType (..))-import qualified GHC.TypeLits.Normalise.Unify as Normalise  -- GHC API import Outputable (Outputable (..), ($$), text)-import TcPluginM  (TcPluginM, matchFam, tcPluginTrace)+import TcPluginM  (TcPluginM, tcPluginTrace) import TcTypeNats (typeNatExpTyCon) import Type       (TyVar, coreView) import TyCoRep    (Type (..), TyLit (..))@@ -40,46 +40,65 @@ -- internal import GHC.TypeLits.Extra.Solver.Operations -normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp+mergeNormResWith+  :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)+  -> MaybeT TcPluginM NormaliseResult+  -> MaybeT TcPluginM NormaliseResult+  -> MaybeT TcPluginM NormaliseResult+mergeNormResWith f x y = do+  (x', n1) <- x+  (y', n2) <- y+  (res, n3) <- f x' y'+  pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3)+++normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1-normaliseNat _ (TyVarTy v)          = pure (V v)-normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)+normaliseNat _ (TyVarTy v)          = pure (V v, Untouched)+normaliseNat _ (LitTy (NumTyLit i)) = pure (I i, Untouched) normaliseNat defs (TyConApp tc [x,y])-  | tc == maxTyCon defs = mergeMax defs <$> normaliseNat defs x-                                        <*> normaliseNat defs y-  | tc == minTyCon defs = mergeMin defs <$> normaliseNat defs x-                                        <*> normaliseNat defs y-  | tc == divTyCon defs = do x' <- normaliseNat defs x-                             y' <- normaliseNat defs y-                             MaybeT (return (mergeDiv x' y'))-  | tc == modTyCon defs = do x' <- normaliseNat defs x-                             y' <- normaliseNat defs y-                             MaybeT (return (mergeMod x' y'))-  | tc == flogTyCon defs = do x' <- normaliseNat defs x-                              y' <- normaliseNat defs y-                              MaybeT (return (mergeFLog x' y'))-  | tc == clogTyCon defs = do x' <- normaliseNat defs x-                              y' <- normaliseNat defs y-                              MaybeT (return (mergeCLog x' y'))-  | tc == logTyCon defs = do x' <- normaliseNat defs x-                             y' <- normaliseNat defs y-                             MaybeT (return (mergeLog x' y'))-  | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x-                                   <*> normaliseNat defs y-  | tc == lcmTyCon defs = mergeLCM <$> normaliseNat defs x-                                   <*> normaliseNat defs y-  | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x-                                     <*> normaliseNat defs y+  | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y'))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == minTyCon defs = mergeNormResWith (\x' y' -> return (mergeMin defs x' y'))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == divTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y')))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == modTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y')))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == flogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y')))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == clogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y')))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == logTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y')))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == gcdTyCon defs = mergeNormResWith (\x' y' -> return (mergeGCD x' y'))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == lcmTyCon defs = mergeNormResWith (\x' y' -> return (mergeLCM x' y'))+                                           (normaliseNat defs x)+                                           (normaliseNat defs y)+  | tc == typeNatExpTyCon = mergeNormResWith (\x' y' -> return (mergeExp x' y'))+                                             (normaliseNat defs x)+                                             (normaliseNat defs y)  normaliseNat defs (TyConApp tc tys) = do-  tys'   <- mapM (fmap (reifyEOP defs) . normaliseNat defs) tys-  tyM    <- lift (matchFam tc tys')-  case tyM of-    Just (_,ty) -> normaliseNat defs ty-    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys')))-         in  return (C (CType (Normalise.reifySOP q)))+  let mergeExtraOp [] = []+      mergeExtraOp ((Just (op, Normalised), _):xs) = reifyEOP defs op:mergeExtraOp xs+      mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs -normaliseNat _ t = return (C (CType t))+  normResults <- lift (sequence (runMaybeT . normaliseNat defs <$> tys))+  let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults)+  let tys' = mergeExtraOp (zip normResults tys)+  pure (C (CType (TyConApp tc tys')), anyNormalised)++normaliseNat _ t = return (C (CType t), Untouched)  -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal.

@@ -97,6 +97,9 @@  testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6) +testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True+testFail27 _ = id+ testFail1Errors =   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"   ,"Actual type: Proxy 4 -> Proxy 4"@@ -214,4 +217,9 @@ testFail26Errors =   ["Could not deduce: Max x y ~ n"   ,"from the context: (x <=? n) ~ 'True"+  ]++testFail27Errors =+  ["Expected type: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"+  ,"Actual type: Proxy 'True -> Proxy 'True"   ]

@@ -191,6 +191,38 @@   -> Proxy (Max 0 (BitPack a) + CLog 2 2) test52 _ = id +test53+  :: Proxy n+  -> Proxy (1 <=? Max (n + 1) 1)+  -> Proxy True+test53 _ = id++test54+  :: Proxy n+  -> Proxy (n <=? Max (n + 1) 1)+  -> Proxy True+test54 _ = id++test55+  :: Proxy n+  -> Proxy (n + 1 <=? Max (n + 1) 1)+  -> Proxy True+test55 _ = id++test56+  :: Proxy n+  -> Proxy p+  -> Proxy (n <=? Max (n + p) p)+  -> Proxy True+test56 _ _ = id++test57+  :: Proxy n+  -> Proxy p+  -> Proxy (n + 1 <=? Max (n + p + 1) p)+  -> Proxy True+test57 _ _ = id+ main :: IO () main = defaultMain tests @@ -353,6 +385,21 @@     , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $       show (test52 Proxy Proxy) @?=       "Proxy"+    , testCase "forall n . 1 <= Max (n + 1) 1" $+      show (test53 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . n <= Max (n + 1) 1" $+      show (test54 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . n + 1 <= Max (n + 1) 1" $+      show (test55 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n p . n <= Max (n + p) p" $+      show (test56 Proxy Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $+      show (test57 Proxy Proxy Proxy) @?=+      "Proxy"     ]   , testGroup "errors"     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors@@ -381,6 +428,7 @@     , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors     , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors     , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors+    , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors     ]   ]