ghc-typelits-natnormalise 0.2.1 → 0.3

raw patch · 9 files changed

+231/−158 lines, 9 filesdep +ghc-tcplugins-extraPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-tcplugins-extra

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• README.md +1/−1
• ghc-typelits-natnormalise.cabal +20/−8
• src/GHC/Extra/Instances.hs +16/−0
• src/GHC/Type/Instances.hs +0/−14
• src/GHC/TypeLits/Normalise.hs +71/−103
• src/GHC/TypeLits/Normalise/Unify.hs +66/−27
• tests/ErrorTests.hs +28/−0
• tests/Tests.hs +22/−5

@@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.3 *June 3rd 2015*+* Find more unifications:+  * `<TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]`+* Fixes bugs:+  * Unifying `a*b ~ b` now returns `[a ~ 1]`; before it erroneously returned `[a ~ ]`, which is interpred as `[a ~ 0]`...+  * Unifying `a+b ~ b` now returns `[a ~ 0]`; before it returned the undesirable, though equal, `[a ~ ]`+ ## 0.2.1 *May 6th 2015* * Update `Eq` instance of `SOP`: Empty SOP is equal to 0 

@@ -1,6 +1,6 @@ # ghc-tynat-normalise -[![Build Status](https://secure.travis-ci.org/christiaanb/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/christiaanb/ghc-typelits-natnormalise)+[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise) 

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.2.1+version:             0.3 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@@ -36,7 +36,7 @@   .   Pragma to the header of your file. homepage:            http://www.clash-lang.org/-bug-reports:         http://github.com/christiaanb/ghc-typelits-natnormalise/issues+bug-reports:         http://github.com/clash-lang/ghc-typelits-natnormalise/issues license:             BSD2 license-file:        LICENSE author:              Christiaan Baaij@@ -50,26 +50,38 @@  source-repository head   type: git-  location: https://github.com/christiaanb/ghc-typelits-natnormalise.git+  location: https://github.com/clash-lang/ghc-typelits-natnormalise.git +flag deverror+  description:+    Enables `-Werror` for development mode and TravisCI+  default: False+  manual: True+ library   exposed-modules:     GHC.TypeLits.Normalise,                        GHC.TypeLits.Normalise.SOP,                        GHC.TypeLits.Normalise.Unify-  Other-Modules:       GHC.Type.Instances+  Other-Modules:       GHC.Extra.Instances   build-depends:       base >=4.8  && <5,-                       ghc  >=7.10 && <7.12+                       ghc  >=7.10 && <7.12,+                       ghc-tcplugins-extra >= 0.1   hs-source-dirs:      src   default-language:    Haskell2010-  ghc-options:         -Wall+  if flag(deverror)+    ghc-options:         -Wall -Werror+  else+    ghc-options:         -Wall -test-suite test-ghc-tynat-normalise+test-suite test-ghc-typelits-natnormalise   type:                exitcode-stdio-1.0   main-is:             Tests.hs+  Other-Modules:       ErrorTests   build-depends:       base >=4.8 && <4.9,                        ghc-typelits-natnormalise >= 0.1,                        tasty >= 0.10,                        tasty-hunit >= 0.9   hs-source-dirs:      tests   default-language:    Haskell2010-  ghc-options:         -O0 -dcore-lint+  if flag(deverror)+    ghc-options:       -O0 -dcore-lint

@@ -0,0 +1,16 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-|+Copyright  :  (C) 2015, University of Twente+License    :  BSD2 (see the file LICENSE)+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>++* 'Eq' instance for 'Ct'++* 'Ord' instance for 'Type' and 'Ct'+-}+module GHC.Extra.Instances where++import Type          (Type,cmpType)++instance Ord Type where+  compare = cmpType

@@ -1,14 +0,0 @@-{-# OPTIONS_GHC -fno-warn-orphans #-}-{-|-Copyright  :  (C) 2015, University of Twente-License    :  BSD2 (see the file LICENSE)-Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>--Ord instance for 'Type'--}-module GHC.Type.Instances where--import Type (Type,cmpType)--instance Ord Type where-  compare = cmpType

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP             #-}+{-# LANGUAGE LambdaCase      #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections   #-} @@ -48,38 +49,27 @@ where  -- external-import Data.Maybe (catMaybes, mapMaybe)+import Data.IORef          (IORef, newIORef,readIORef, modifyIORef)+import Data.Maybe          (catMaybes, mapMaybe)+import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, newGiven,+                            newWantedWithProvenance, tracePlugin)  -- GHC API-import Coercion   (Role (Nominal), mkUnivCo)-import FastString (fsLit)-import Outputable (Outputable (..), (<+>), ($$), empty, text)+import Outputable (Outputable (..), (<+>), ($$), text) import Plugins    (Plugin (..), defaultPlugin)-import TcEvidence (EvTerm (EvCoercion), TcCoercion (..))-import TcPluginM  (TcPluginM, tcPluginTrace, unsafeTcPluginTcM, zonkCt)-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711-import qualified  Inst-#else-import qualified  TcMType-#endif-import TcRnTypes  (Ct, CtLoc, CtOrigin, TcPlugin(..),-                   TcPluginResult(..), ctEvidence, ctEvPred,-                   ctLoc, ctLocOrigin, isGiven, isWanted, mkNonCanonical)-import TcSMonad   (runTcS,newGivenEvVar)+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), PredType, Type,-                   TyVar, classifyPredType, mkTyVarTy)+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), Type, TyVar,+                   classifyPredType, mkTyVarTy) import TysWiredIn (typeNatKind)  -- internal+import GHC.Extra.Instances () -- Ord instance for Ct import GHC.TypeLits.Normalise.Unify --- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301-import Control.Monad (unless)-import Data.IORef    (readIORef)-import StaticFlags   (initStaticOpts, v_opt_C_ready)-import TcPluginM     (tcPluginIO)- -- | To use the plugin, add -- -- @@@ -92,14 +82,15 @@  normalisePlugin :: TcPlugin normalisePlugin = tracePlugin "ghc-typelits-natnormalise"-  TcPlugin { tcPluginInit  = return ()+  TcPlugin { tcPluginInit  = tcPluginIO $ newIORef []            , tcPluginSolve = decideEqualSOP            , tcPluginStop  = const (return ())            } -decideEqualSOP :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-decideEqualSOP _ _givens _deriveds []      = return (TcPluginOk [] [])-decideEqualSOP _ givens  _deriveds wanteds = do+decideEqualSOP :: IORef [Ct] -> [Ct] -> [Ct] -> [Ct]+               -> TcPluginM TcPluginResult+decideEqualSOP _          _givens _deriveds []      = return (TcPluginOk [] [])+decideEqualSOP discharged givens  _deriveds wanteds = do     -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out     let wanteds' = filter (isWanted . ctEvidence) wanteds     let unit_wanteds = mapMaybe toNatEquality wanteds'@@ -110,39 +101,69 @@         sr <- simplifyNats (unit_givens ++ unit_wanteds)         tcPluginTrace "normalised" (ppr sr)         case sr of-          Simplified subst evs ->-            TcPluginOk (filter (isWanted . ctEvidence . snd) evs) <$>-              mapM substItemToCt (filter (isWanted . ctEvidence . siNote) subst)-          Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq])+          Simplified subst evs -> do+            let solved     = filter (isWanted . ctEvidence . snd) evs+            -- Create new wanted constraints+            let newWanteds = filter (isWanted . ctEvidence . siNote) subst+            discharedWanteds <- tcPluginIO (readIORef discharged)+            let existingWanteds = wanteds' ++ discharedWanteds+            newWantedConstraints <- catMaybes <$>+                                    mapM (substItemToCt existingWanteds)+                                         newWanteds+            -- update set of discharged wanteds+            tcPluginIO (modifyIORef discharged (++ newWantedConstraints))+            -- return+            return (TcPluginOk solved newWantedConstraints)+          Impossible eq -> failWithProvenace $ fromNatEquality eq -substItemToCt :: SubstItem TyVar Type Ct -> TcPluginM Ct-substItemToCt si-  | isGiven (ctEvidence ct) = newSimpleGiven loc predicate (ty1,ty2)-  | otherwise               = newSimpleWanted (ctLocOrigin loc) predicate+substItemToCt :: [Ct] -- ^ Existing wanteds wanted+              -> UnifyItem TyVar Type Ct+              -> TcPluginM (Maybe Ct)+substItemToCt existingWanteds si+  | isGiven (ctEvidence ct)+  = Just <$> mkNonCanonical <$> newGiven loc predicate evTm++  -- Only create new wanteds+  | predicate  `notElem` wantedPreds+  , predicateS `notElem` wantedPreds+  = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate++  | otherwise+  = return Nothing   where-    predicate = mkEqPred ty1 ty2-    ty1  = mkTyVarTy (siVar si)-    ty2  = reifySOP (siSOP si)-    ct   = siNote si-    loc  = ctLoc ct+    predicate   = mkEqPred ty1 ty2+    predicateS  = mkEqPred ty2 ty1+    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+ type NatEquality = (Ct,CoreSOP,CoreSOP)  fromNatEquality :: NatEquality -> Ct fromNatEquality (ct, _, _) = ct  data SimplifyResult-  = Simplified CoreSubst [(EvTerm,Ct)]+  = Simplified CoreUnify [(EvTerm,Ct)]   | Impossible NatEquality  instance Outputable SimplifyResult where   ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs   ppr (Impossible eq)  = text "Impossible" <+> ppr eq -simplifyNats :: [NatEquality] -> TcPluginM SimplifyResult-simplifyNats eqs = tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs+simplifyNats :: [NatEquality]+             -> TcPluginM SimplifyResult+simplifyNats eqs =+    tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs   where-    simples :: CoreSubst -> [Maybe (EvTerm, Ct)] -> [NatEquality]+    simples :: CoreUnify -> [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@@ -151,10 +172,11 @@       case ur of         Win         -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []                                (xs ++ eqs')-        Lose        -> return  (Impossible eq)+        Lose        -> return (Impossible eq)         Draw []     -> simples subst evs (eq:xs) eqs'-        Draw subst' -> simples (substsSubst subst' subst ++ subst') evs [eq]-                               (xs ++ eqs')+        Draw subst' -> simples (substsSubst subst' subst ++ subst')+                               (((,) <$> evMagic ct <*> pure ct):evs)+                               [] (xs ++ eqs')  -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe NatEquality@@ -167,61 +189,7 @@     isNatKind :: Kind -> Bool     isNatKind = (== typeNatKind) --- Utils-newSimpleWanted :: CtOrigin -> PredType -> TcPluginM Ct-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711-newSimpleWanted orig = fmap mkNonCanonical . unsafeTcPluginTcM . Inst.newWanted orig-#else-newSimpleWanted orig = unsafeTcPluginTcM . TcMType.newSimpleWanted orig-#endif--newSimpleGiven :: CtLoc -> PredType -> (Type,Type) -> TcPluginM Ct-newSimpleGiven loc predicate (ty1,ty2)= do-  (ev,_) <- unsafeTcPluginTcM $ runTcS-                              $ newGivenEvVar loc-                                  (predicate, evByFiat "units" (ty1, ty2))-  return (mkNonCanonical ev)- evMagic :: Ct -> Maybe EvTerm evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of-    EqPred NomEq t1 t2 -> Just (evByFiat "tylits_magic" (t1, t2))-    _                  -> Nothing--evByFiat :: String -> (Type, Type) -> EvTerm-evByFiat name (t1,t2) = EvCoercion $ TcCoercion-                      $ mkUnivCo (fsLit name) Nominal t1 t2--tracePlugin :: String -> TcPlugin -> TcPlugin-tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit  = traceInit-                                      , tcPluginSolve = traceSolve-                                      , tcPluginStop  = traceStop-                                      }-  where-    traceInit    = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301-                      initializeStaticFlags-                      tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit-    traceStop  z = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301-                      initializeStaticFlags-                      tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z--    traceSolve z given derived wanted = do-        -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301-        initializeStaticFlags-        tcPluginTrace ("tcPluginSolve start " ++ s)-                          (text "given   =" <+> ppr given-                        $$ text "derived =" <+> ppr derived-                        $$ text "wanted  =" <+> ppr wanted)-        r <- tcPluginSolve z given derived wanted-        case r of-          TcPluginOk solved new     -> tcPluginTrace ("tcPluginSolve ok " ++ s)-                                           (text "solved =" <+> ppr solved-                                         $$ text "new    =" <+> ppr new)-          TcPluginContradiction bad -> tcPluginTrace ("tcPluginSolve contradiction " ++ s)-                                           (text "bad =" <+> ppr bad)-        return r---- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301-initializeStaticFlags :: TcPluginM ()-initializeStaticFlags = tcPluginIO $ do-  r <- readIORef v_opt_C_ready-  unless r initStaticOpts+  EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2)+  _                  -> Nothing

@@ -1,3 +1,4 @@+{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -fno-warn-unused-imports #-}  {-|@@ -11,9 +12,9 @@   , normaliseNat   , reifySOP     -- * Substitution on 'SOP' terms-  , SubstItem (..)-  , TySubst-  , CoreSubst+  , UnifyItem (..)+  , TyUnify+  , CoreUnify   , substsSOP   , substsSubst     -- * Find unifiers@@ -41,7 +42,7 @@                       unitUniqSet)  -- Internal-import GHC.Type.Instances () -- Ord instance for Type+import GHC.Extra.Instances () -- Ord instance for Type import GHC.TypeLits.Normalise.SOP  -- Used for haddock@@ -104,21 +105,27 @@ -- | 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 CoreSubst     = TySubst TyVar Type Ct-type TySubst v c n = [SubstItem v c n]+type CoreUnify     = TyUnify TyVar Type Ct+type TyUnify v c n = [UnifyItem v c n] -data SubstItem v c n = SubstItem { siVar  :: v+data UnifyItem v c n = SubstItem { siVar  :: v                                  , siSOP  :: SOP v c                                  , siNote :: n                                  }+                     | UnifyItem { siLHS  :: SOP v c+                                 , siRHS  :: SOP v c+                                 , siNote :: n+                                 } -instance (Outputable v, Outputable c) => Outputable (SubstItem v c n) where-  ppr si = ppr (siVar si) <+> text " := " <+> ppr (siSOP si)+instance (Outputable v, Outputable c) => Outputable (UnifyItem v c n) where+  ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP+  ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS  -- | Apply a substitution to a single normalised 'SOP' term-substsSOP :: (Ord v, Ord c) => TySubst v c n -> SOP v c -> SOP v c-substsSOP []     u = u-substsSOP (si:s) u = substsSOP s (substSOP (siVar si) (siSOP si) u)+substsSOP :: (Ord v, Ord c) => TyUnify v c n -> 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 tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS@@ -135,15 +142,18 @@ 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) => TySubst v c n -> TySubst v c n -> TySubst v c n-substsSubst s = map (\si -> si {siSOP = substsSOP s (siSOP si)})+substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n+substsSubst s = map subt+  where+    subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}+    subt si@(UnifyItem {..}) = si {siLHS = substsSOP s siLHS, siRHS = substsSOP s siRHS}  -- | 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 CoreSubst -- ^ Two terms are only equal if the given substitution holds+  | Draw CoreUnify -- ^ Two terms are only equal if the given substitution holds  instance Outputable UnifyResult where   ppr Win          = text "Win"@@ -162,8 +172,12 @@  unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v-    | eqFV u v  = if u == v then Win else Lose-    | otherwise = Draw (unifiers 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)  -- | Find unifiers for two SOP terms --@@ -198,30 +212,46 @@ -- @ -- [a := b] -- @-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreSubst+unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify unifiers ct (S [P [V x]]) s-  | isGiven (ctEvidence ct) = [SubstItem x s     ct]+  | isGiven (ctEvidence ct) = [SubstItem x s ct]   | otherwise               = [] unifiers ct s (S [P [V x]])-  | isGiven (ctEvidence ct) = [SubstItem x s     ct]+  | isGiven (ctEvidence ct) = [SubstItem x s ct]   | otherwise               = []+unifiers _ (S [P [C _]]) _  = []+unifiers _ _ (S [P [C _]])  = [] unifiers ct u v             = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreSubst+unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify 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] -unifiers' ct (S [P [V x]]) s             = [SubstItem x s     ct]-unifiers' ct s             (S [P [V x]]) = [SubstItem x s     ct]+unifiers' ct (S [P [V x]]) s             = [SubstItem x s ct]+unifiers' ct s             (S [P [V x]]) = [SubstItem x s ct] +unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct]+unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]+ -- (3 * a) ~ 0 ==> [a := 0] unifiers' ct (S [P ((I _):ps)]) (S [P [I 0]]) = unifiers' ct (S [P ps]) (S [P [I 0]]) unifiers' ct (S [P [I 0]]) (S [P ((I _):ps)]) = unifiers' ct (S [P ps]) (S [P [I 0]])  -- (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 (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''])+  where+    ps1'  = ps1 \\ psx+    ps2'  = ps2 \\ psx+    ps1'' | null ps1' = [I 1]+          | otherwise = ps1'+    ps2'' | null ps2' = [I 1]+          | otherwise = ps2'+    psx  = intersect ps1 ps2  -- (2 + a) ~ 5 ==> [a := 3] unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))@@ -231,8 +261,14 @@ -- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1)       (S ps2)     | null psx  = []-    | otherwise = unifiers' ct (S (ps1 \\ psx)) (S (ps2 \\ psx))+    | otherwise = unifiers' ct (S ps1'') (S ps2'')   where+    ps1'  = ps1 \\ psx+    ps2'  = ps2 \\ psx+    ps1'' | null ps1' = [P [I 0]]+          | otherwise = ps1'+    ps2'' | null ps2' = [P [I 0]]+          | otherwise = ps2'     psx = intersect ps1 ps2  -- | Find the 'TyVar' in a 'CoreSOP'@@ -250,3 +286,6 @@  eqFV :: CoreSOP -> CoreSOP -> Bool eqFV = (==) `on` fvSOP++containsConstants :: CoreSOP -> Bool+containsConstants = any (any (\c -> case c of {(C _) -> True; _ -> False}) . unP) . unS

@@ -0,0 +1,28 @@+{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}++{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+module ErrorTests where++import Data.Proxy+import GHC.TypeLits++testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)+testProxy1 = id++testProxy1Errors =+  ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"+  ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"+  ]++type family GCD (x :: Nat) (y :: Nat) :: Nat+type instance GCD 6 8 = 2+type instance GCD 9 6 = 3++testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)+testProxy2 = id++testProxy2Errors =+  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"+  ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"+  ]

@@ -1,8 +1,9 @@-{-# LANGUAGE DataKinds         #-}-{-# LANGUAGE GADTs             #-}-{-# LANGUAGE KindSignatures    #-}-{-# LANGUAGE TypeOperators     #-}-{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE NoImplicitPrelude   #-}+{-# LANGUAGE ScopedTypeVariables #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -12,9 +13,13 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P +import Data.List (isInfixOf)+import Control.Exception import Test.Tasty import Test.Tasty.HUnit +import ErrorTests+ data Vec :: Nat -> * -> * where   Nil  :: Vec 0 a   (:>) :: a -> Vec n a -> Vec (n + 1) a@@ -256,4 +261,16 @@       show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?=       "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>"     ]+  , testGroup "errors"+    [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors+    , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors+    ]   ]++-- | Assert that evaluation of the first argument (to WHNF) will throw+-- 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