ghc-typelits-natnormalise 0.3.1 → 0.4

raw patch · 9 files changed

+274/−69 lines, 9 filesdep ~basedep ~ghcdep ~ghc-tcplugins-extraPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, ghc, ghc-tcplugins-extra, ghc-typelits-natnormalise

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• LICENSE +1/−1
• ghc-typelits-natnormalise.cabal +17/−6
• src/GHC/Extra/Instances.hs +14/−3
• src/GHC/TypeLits/Normalise.hs +112/−29
• src/GHC/TypeLits/Normalise/SOP.hs +4/−1
• src/GHC/TypeLits/Normalise/Unify.hs +74/−24
• tests/ErrorTests.hs +22/−0
• tests/Tests.hs +20/−5

@@ -1,5 +1,15 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4 *January 19th 2016*+* Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only)+* Find more unifications:+  * `F x + 2 - 1 - 1 ~ F x` ==> [F x := F x], where `F` can be any type function with result `Nat`.++## 0.3.2+* Find more unifications:+  * `(z ^ a) ~ (z ^ b) ==> [a := b]`+  * `(i ^ a) ~ j ==> [a := round (logBase i j)]`, when `i` and `j` are integers, and `ceiling (logBase i j) == floor (logBase i j)`.+ ## 0.3.1 *October 19th 2015* * Find more unifications:   * `(i * a) ~ j ==> [a := div j i]`, when `i` and `j` are integers, and `mod j i == 0`.

@@ -1,4 +1,4 @@-Copyright (c) 2015, University of Twente+Copyright (c) 2015-2016, University of Twente All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.3.1+version:             0.4 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ of types of kind@@ -41,7 +41,7 @@ license-file:        LICENSE author:              Christiaan Baaij maintainer:          christiaan.baaij@gmail.com-copyright:           Copyright © 2015 University of Twente+copyright:           Copyright © 2015-2016 University of Twente category:            Type System build-type:          Simple extra-source-files:  README.md@@ -64,10 +64,14 @@                        GHC.TypeLits.Normalise.Unify   Other-Modules:       GHC.Extra.Instances   build-depends:       base >=4.8  && <5,-                       ghc  >=7.10 && <7.12,-                       ghc-tcplugins-extra >= 0.1+                       ghc  >=7.10 && <8.2,+                       ghc-tcplugins-extra >= 0.2   hs-source-dirs:      src   default-language:    Haskell2010+  other-extensions:    CPP+                       LambdaCase+                       RecordWildCards+                       TupleSections   if flag(deverror)     ghc-options:         -Wall -Werror   else@@ -77,11 +81,18 @@   type:                exitcode-stdio-1.0   main-is:             Tests.hs   Other-Modules:       ErrorTests-  build-depends:       base >=4.8 && <4.9,-                       ghc-typelits-natnormalise >= 0.1,+  build-depends:       base >=4.8 && <5,+                       ghc-typelits-natnormalise >= 0.4,                        tasty >= 0.10,                        tasty-hunit >= 0.9   hs-source-dirs:      tests   default-language:    Haskell2010+  other-extensions:    DataKinds+                       GADTs+                       KindSignatures+                       NoImplicitPrelude+                       TypeFamilies+                       TypeOperators+                       ScopedTypeVariables   if flag(deverror)     ghc-options:       -O0 -dcore-lint

@@ -1,6 +1,5 @@-{-# OPTIONS_GHC -fno-warn-orphans #-} {-|-Copyright  :  (C) 2015, University of Twente+Copyright  :  (C) 2015-2016, University of Twente License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> @@ -8,9 +7,21 @@  * 'Ord' instance for 'Type' and 'Ct' -}++{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+ module GHC.Extra.Instances where -import Type          (Type,cmpType)+import Type (Type,cmpType)+#if __GLASGOW_HASKELL__ >= 711+import Type (eqType)+#endif++#if __GLASGOW_HASKELL__ >= 711+instance Eq Type where+  (==) = eqType+#endif  instance Ord Type where   compare = cmpType

@@ -1,12 +1,5 @@-{-# LANGUAGE CPP             #-}-{-# LANGUAGE LambdaCase      #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections   #-}--{-# OPTIONS_HADDOCK show-extensions #-}- {-|-Copyright  :  (C) 2015, University of Twente+Copyright  :  (C) 2015-2016, University of Twente License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> @@ -44,6 +37,18 @@  To the header of your file. -}++{-# LANGUAGE CPP             #-}+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections   #-}++{-# OPTIONS_HADDOCK show-extensions #-}++#if __GLASGOW_HASKELL__ < 711+{-# OPTIONS_GHC -fno-warn-deprecations #-}+#endif+ module GHC.TypeLits.Normalise   ( plugin ) where@@ -51,21 +56,33 @@ -- external import Data.IORef          (IORef, newIORef,readIORef, modifyIORef) import Data.Maybe          (catMaybes, mapMaybe)-import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, newGiven,-                            newWantedWithProvenance, tracePlugin)+import GHC.TcPluginM.Extra (evByFiat, newGiven, tracePlugin)  -- GHC API import Outputable (Outputable (..), (<+>), ($$), text) import Plugins    (Plugin (..), defaultPlugin)-import TcEvidence (EvTerm)+import TcEvidence (EvTerm (..)) import TcPluginM  (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt) import TcRnTypes  (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,                    ctPred, ctLoc, isGiven, isWanted, mkNonCanonical)-import TcType     (mkEqPred, typeKind)-import Type       (EqRel (NomEq), Kind, PredTree (EqPred), Type, TyVar,-                   classifyPredType, mkTyVarTy)+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, TyVar,+                   classifyPredType, getEqPredTys, mkTyVarTy) import TysWiredIn (typeNatKind) +#if __GLASGOW_HASKELL__ >= 711+import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,+                   mkNomReflCo, mkUnivCo)+import TcPluginM  (newCoercionHole, newFlexiTyVar)+import TcRnTypes  (CtEvidence (..), TcEvDest (..))+import TyCoRep    (UnivCoProvenance (..))+import Type       (mkPrimEqPred)+import TcType     (typeKind)+#else+import TcType              (mkEqPred, typeKind)+import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace)+#endif++ -- internal import GHC.Extra.Instances () -- Ord instance for Ct import GHC.TypeLits.Normalise.Unify@@ -104,7 +121,11 @@           Simplified subst evs -> do             let solved     = filter (isWanted . ctEvidence . snd) evs             -- Create new wanted constraints+#if __GLASGOW_HASKELL__ >= 711+            let newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst+#else             let newWanteds = filter (isWanted . ctEvidence . siNote) subst+#endif             discharedWanteds <- tcPluginIO (readIORef discharged)             let existingWanteds = wanteds' ++ discharedWanteds             newWantedConstraints <- catMaybes <$>@@ -114,10 +135,14 @@             tcPluginIO (modifyIORef discharged (++ newWantedConstraints))             -- return             return (TcPluginOk solved newWantedConstraints)-          Impossible eq -> failWithProvenace $ fromNatEquality eq+#if __GLASGOW_HASKELL__ >= 711+          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])+#else+          Impossible eq -> failWithProvenace (fromNatEquality eq)+#endif  substItemToCt :: [Ct] -- ^ Existing wanteds wanted-              -> UnifyItem TyVar Type Ct+              -> UnifyItem TyVar Type CoreNote               -> TcPluginM (Maybe Ct) substItemToCt existingWanteds si   | isGiven (ctEvidence ct)@@ -126,32 +151,57 @@   -- Only create new wanteds   | predicate  `notElem` wantedPreds   , predicateS `notElem` wantedPreds+#if __GLASGOW_HASKELL__ >= 711+  = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) loc)))+#else   = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate+#endif    | otherwise   = return Nothing   where-    predicate   = mkEqPred ty1 ty2+    predicate   = unifyItemToPredType si+    (ty1,ty2)   = getEqPredTys predicate+#if __GLASGOW_HASKELL__ >= 711+    predicateS    = mkPrimEqPred ty2 ty1+    ((ev,_,_),ct) = siNote si+#else     predicateS  = mkEqPred ty2 ty1+    ct          = siNote si+#endif     wantedPreds = map ctPred existingWanteds -    ty1       = case si of-                  (SubstItem {..}) -> mkTyVarTy siVar-                  (UnifyItem {..}) -> reifySOP siLHS-    ty2       = case si of-                  (SubstItem {..}) -> reifySOP siSOP-                  (UnifyItem {..}) -> reifySOP siRHS-    ct        = siNote si     loc       = ctLoc ct     evTm      = evByFiat "ghc-typelits-natnormalise" ty1 ty2 +unifyItemToPredType :: UnifyItem TyVar Type a -> PredType+unifyItemToPredType ui =+#if __GLASGOW_HASKELL__ >= 711+    mkPrimEqPred ty1 ty2+#else+    mkEqPred ty1 ty2+#endif+  where+    ty1 = case ui of+            SubstItem {..} -> mkTyVarTy siVar+            UnifyItem {..} -> reifySOP siLHS+    ty2 = case ui of+            SubstItem {..} -> reifySOP siSOP+            UnifyItem {..} -> reifySOP siRHS+ type NatEquality = (Ct,CoreSOP,CoreSOP)  fromNatEquality :: NatEquality -> Ct fromNatEquality (ct, _, _) = ct +#if __GLASGOW_HASKELL__ >= 711+type CoreNote = ((CoercionHole,TyVar,PredType), Ct)+#else+type CoreNote = Ct+#endif+ data SimplifyResult-  = Simplified CoreUnify [(EvTerm,Ct)]+  = Simplified (CoreUnify CoreNote) [(EvTerm,Ct)]   | Impossible NatEquality  instance Outputable SimplifyResult where@@ -163,20 +213,38 @@ simplifyNats eqs =     tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs   where-    simples :: CoreUnify -> [Maybe (EvTerm, Ct)] -> [NatEquality]+    simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct)] -> [NatEquality]             -> [NatEquality] -> TcPluginM SimplifyResult     simples subst evs _xs [] = return (Simplified subst (catMaybes evs))     simples subst evs xs (eq@(ct,u,v):eqs') = do       ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)       tcPluginTrace "unifyNats result" (ppr ur)       case ur of+#if __GLASGOW_HASKELL__ >= 711+        Win         -> simples subst (((,) <$> evMagic ct [] <*> pure ct):evs) []+                               (xs ++ eqs')+        Lose        -> return (Impossible eq)+        Draw []     -> simples subst evs (eq:xs) eqs'+        Draw subst' -> do+          newEvs <- mapM (\si -> (,,) <$> newCoercionHole+                                      <*> newFlexiTyVar typeNatKind+                                      <*> pure (unifyItemToPredType si))+                         subst'+          let subst'' = zipWith (\si ev -> si {siNote = (ev,siNote si)})+                                subst' newEvs+          simples (substsSubst subst'' subst ++ subst'')+            (((,) <$> evMagic ct newEvs <*> pure ct):evs)+            [] (xs ++ eqs')+#else         Win         -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []                                (xs ++ eqs')         Lose        -> return (Impossible eq)         Draw []     -> simples subst evs (eq:xs) eqs'-        Draw subst' -> simples (substsSubst subst' subst ++ subst')-                               (((,) <$> evMagic ct <*> pure ct):evs)-                               [] (xs ++ eqs')+        Draw subst' -> do+          simples (substsSubst subst' subst ++ subst')+                  (((,) <$> evMagic ct <*> pure ct):evs)+                  [] (xs ++ eqs')+#endif  -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe NatEquality@@ -189,7 +257,22 @@     isNatKind :: Kind -> Bool     isNatKind = (== typeNatKind) +#if __GLASGOW_HASKELL__ >= 711+evMagic :: Ct -> [(CoercionHole, TyVar, PredType)] -> Maybe EvTerm+evMagic ct evs = case classifyPredType $ ctEvPred $ ctEvidence ct of+  EqPred NomEq t1 t2 ->+    let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2+        (holes,tvs,preds) = unzip3 evs+        holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p))+                          holes preds+        natReflCo = mkNomReflCo typeNatKind+        forallEv = mkForAllCos (map (,natReflCo) tvs) ctEv+        finalEv = foldl mkInstCo forallEv holeEvs+    in  Just (EvCoercion finalEv)+  _ -> Nothing+#else evMagic :: Ct -> Maybe EvTerm evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of   EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2)   _                  -> Nothing+#endif

@@ -1,5 +1,5 @@ {-|-Copyright  :  (C) 2015, University of Twente+Copyright  :  (C) 2015-2016, University of Twente License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> @@ -284,10 +284,12 @@   . mergeWith mergeP   . map (P . sort . map reduceExp . mergeWith mergeS . unP)   . unS+{-# INLINEABLE simplifySOP #-}  -- | Merge two SOP terms by additions mergeSOPAdd :: (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@@ -295,3 +297,4 @@   = simplifySOP   . S   $ concatMap (zipWith (\p1 p2 -> P (unP p1 ++ unP p2)) sop1 . repeat) sop2+{-# INLINEABLE mergeSOPMul #-}

@@ -1,11 +1,13 @@-{-# LANGUAGE RecordWildCards #-}-{-# OPTIONS_GHC -fno-warn-unused-imports #-}- {-|-Copyright  :  (C) 2015, University of Twente+Copyright  :  (C) 2015-2016, University of Twente License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> -}++{-# LANGUAGE CPP             #-}+{-# LANGUAGE RecordWildCards #-}+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+ module GHC.TypeLits.Normalise.Unify   ( -- * 'Nat' expressions \<-\> 'SOP' terms     CoreSOP@@ -34,10 +36,16 @@ import Outputable    (Outputable (..), (<+>), ($$), text) import TcPluginM     (TcPluginM, tcPluginTrace) import TcRnMonad     (Ct, ctEvidence, isGiven)+import TcRnTypes     (ctEvPred) import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,                       typeNatSubTyCon)-import Type          (TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy, tcView)+import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,+                      coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)+#if __GLASGOW_HASKELL__ >= 711+import TyCoRep       (Type (..), TyLit (..))+#else import TypeRep       (Type (..), TyLit (..))+#endif import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,                       unitUniqSet) @@ -60,7 +68,7 @@ -- * type variables -- * Applications of the arithmetic operators @(+,-,*,^)@ normaliseNat :: Type -> CoreSOP-normaliseNat ty | Just ty1 <- tcView ty = normaliseNat ty1+normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1 normaliseNat (TyVarTy v)          = S [P [V v]] normaliseNat (LitTy (NumTyLit i)) = S [P [I i]] normaliseNat (TyConApp tc [x,y])@@ -105,7 +113,8 @@ -- | 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.-type CoreUnify     = TyUnify TyVar Type Ct+type CoreUnify a = TyUnify TyVar Type a+ type TyUnify v c n = [UnifyItem v c n]  data UnifyItem v c n = SubstItem { siVar  :: v@@ -147,13 +156,14 @@   where     subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}     subt si@(UnifyItem {..}) = si {siLHS = substsSOP s siLHS, siRHS = substsSOP s siRHS}+{-# INLINEABLE substsSubst #-}  -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal. data UnifyResult   = Win            -- ^ Two terms are equal   | Lose           -- ^ Two terms are /not/ equal-  | Draw CoreUnify -- ^ Two terms are only equal if the given substitution holds+  | Draw (CoreUnify Ct) -- ^ Two terms are only equal if the given substitution holds  instance Outputable UnifyResult where   ppr Win          = text "Win"@@ -172,12 +182,15 @@  unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v-  | eqFV u v-  , not (containsConstants u)-  , not (containsConstants v)-  = if u == v then Win else Lose-  | otherwise-  = Draw (unifiers ct u v)+  = if eqFV u v+       then if containsConstants u || containsConstants v+               then if u == v+                       then Win+                       else Draw (unifiers ct u v)+               else if u == v+                       then Win+                       else Lose+       else Draw (unifiers ct u v)  -- | Find unifiers for two SOP terms --@@ -212,18 +225,30 @@ -- @ -- [a := b] -- @-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify-unifiers ct (S [P [V x]]) s-  | isGiven (ctEvidence ct) = [SubstItem x s ct]-  | otherwise               = []-unifiers ct s (S [P [V x]])-  | isGiven (ctEvidence ct) = [SubstItem x s ct]-  | otherwise               = []-unifiers _ (S [P [C _]]) _  = []-unifiers _ _ (S [P [C _]])  = []+unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct+unifiers ct u@(S [P [V x]]) v+  = case classifyPredType $ ctEvPred $ ctEvidence ct of+      EqPred NomEq t1 _+        | reifySOP u /= t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct]+      _ -> []+unifiers ct u v@(S [P [V x]])+  = case classifyPredType $ ctEvPred $ ctEvidence ct of+      EqPred NomEq _ t2+        | reifySOP v /= t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct]+      _ -> []+unifiers ct u@(S [P [C _]]) v+  = case classifyPredType $ ctEvPred $ ctEvidence ct of+      EqPred NomEq t1 t2+        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]+      _ -> []+unifiers ct u v@(S [P [C _]])+  = case classifyPredType $ ctEvPred $ ctEvidence ct of+      EqPred NomEq t1 t2+        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]+      _ -> [] unifiers ct u v             = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify+unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct unifiers' ct (S [P [V x]]) (S [])        = [SubstItem x (S [P [I 0]]) ct] unifiers' ct (S [])        (S [P [V x]]) = [SubstItem x (S [P [I 0]]) ct] @@ -232,6 +257,31 @@  unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct] unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]+++-- (z ^ a) ~ (z ^ b) ==> [a := b]+unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])+  | s1 == s2 = unifiers' ct (S [p1]) (S [p2])++-- (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]])+    = if kC == kF+         then unifiers' ct (S [p]) (S [P [I kC]])+         else []+  where+    k  = logBase (fromInteger i :: Double) (fromInteger j)+    kC = ceiling k :: Integer+    kF = floor k :: Integer++unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]])+    = if kC == kF+         then unifiers' ct (S [p]) (S [P [I kC]])+         else []+  where+    k  = logBase (fromInteger i :: Double) (fromInteger j)+    kC = ceiling k :: Integer+    kF = floor k :: Integer  -- (i * a) ~ j ==> [a := div j i] -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0

@@ -56,3 +56,25 @@   ["Expected type: Proxy 7 -> ()"   ,"Actual type: Proxy ((2 * y1) + 4) -> ()"   ]++proxyFun6 :: Proxy (2^k) -> Proxy (2^k)+proxyFun6 = const Proxy++testProxy6 :: Proxy 7+testProxy6 = proxyFun6 (Proxy :: Proxy 7)++testProxy6Errors =+  ["Expected type: Proxy (2 ^ k0)"+  ,"Actual type: Proxy 7"+  ]++proxyFun7 :: Proxy (2^k) -> Proxy k+proxyFun7 = const Proxy++testProxy8 :: Proxy x -> Proxy (y + x)+testProxy8 = id++testProxy8Errors =+  ["Expected type: Proxy x -> Proxy (y + x)"+  ,"Actual type: Proxy x -> Proxy x"+  ]

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP                 #-} {-# LANGUAGE DataKinds           #-} {-# LANGUAGE GADTs               #-} {-# LANGUAGE KindSignatures      #-}@@ -7,13 +8,13 @@  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -import Data.Proxy import GHC.TypeLits import Unsafe.Coerce import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P  import Data.List (isInfixOf)+import Data.Proxy import Control.Exception import Test.Tasty import Test.Tasty.HUnit@@ -27,7 +28,7 @@ instance Show a => Show (Vec n a) where   show vs = "<" P.++ punc vs P.++ ">"     where-      punc :: Show a => Vec m a -> String+      punc :: Vec m a -> String       punc Nil        = ""       punc (x :> Nil) = show x       punc (x :> xs)  = show x P.++ "," P.++ punc xs@@ -266,6 +267,9 @@     , testCase "show (proxyFun4 (Proxy :: Proxy 8))" $       show (proxyFun4 (Proxy :: Proxy 8)) @?=       "()"+    , testCase "show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3)" $+      show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3) @?=+      "Proxy"     ]   , testGroup "errors"     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors@@ -273,6 +277,8 @@     , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors     , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors     , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors+    , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors+    , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors     ]   ] @@ -280,6 +286,15 @@ -- an exception whose string representation contains the given -- substrings. throws :: a -> [String] -> Assertion-throws v xs =-  (evaluate v >> assertFailure "No exception!")-  `catch` \ (e :: SomeException) -> if all (`isInfixOf` show e) xs then return () else throw e+throws v xs = do+  result <- try (evaluate v)+  case result of+    Right _ -> assertFailure "No exception!"+#if MIN_VERSION_base(4,9,0)+    Left (TypeError msg) ->+#else+    Left (ErrorCall msg) ->+#endif+      if all (`isInfixOf` msg) xs+         then return ()+         else assertFailure msg