ghc-typelits-natnormalise 0.5 → 0.5.1
raw patch · 6 files changed
+154/−146 lines, 6 filesdep +template-haskell
Dependencies added: template-haskell
Files
- CHANGELOG.md +4/−0
- ghc-typelits-natnormalise.cabal +4/−2
- src/GHC/TypeLits/Normalise.hs +66/−97
- src/GHC/TypeLits/Normalise/Unify.hs +34/−35
- tests/ErrorTests.hs +45/−12
- tests/Tests.hs +1/−0
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.1 *September 29th 2016*+* Fixes bugs:+ * Cannot solve an equality for the second time in a definition group+ ## 0.5 *August 17th 2016* * Solve simple inequalities, i.e.: * `a <= a + 1`
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.5+version: 0.5.1 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@@ -84,13 +84,15 @@ build-depends: base >=4.8 && <5, ghc-typelits-natnormalise >= 0.4, tasty >= 0.10,- tasty-hunit >= 0.9+ tasty-hunit >= 0.9,+ template-haskell >= 2.11.0.0 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds GADTs KindSignatures NoImplicitPrelude+ TemplateHaskell TypeFamilies TypeOperators ScopedTypeVariables
src/GHC/TypeLits/Normalise.hs view
@@ -50,26 +50,26 @@ -- external import Control.Arrow (second)-import Data.IORef (IORef, newIORef,readIORef, modifyIORef)+import Control.Monad (replicateM) import Data.List (intersect)-import Data.Maybe (catMaybes, mapMaybe)+import Data.Maybe (mapMaybe) import GHC.TcPluginM.Extra (tracePlugin) -- GHC API import Outputable (Outputable (..), (<+>), ($$), text) import Plugins (Plugin (..), defaultPlugin) import TcEvidence (EvTerm (..))-import TcPluginM (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt)+import TcPluginM (TcPluginM, tcPluginTrace, zonkCt) import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,- ctPred, isWanted, mkNonCanonical)-import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, TyVar,+ isWanted, mkNonCanonical)+import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, classifyPredType, eqType, getEqPredTys, mkTyVarTy) import TysWiredIn (typeNatKind) import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo, mkNomReflCo, mkUnivCo) import TcPluginM (newCoercionHole, newFlexiTyVar)-import TcRnTypes (CtEvidence (..), TcEvDest (..), ctLoc)+import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc) import TyCoRep (UnivCoProvenance (..)) import Type (mkPrimEqPred) import TcType (typeKind)@@ -96,15 +96,15 @@ normalisePlugin :: TcPlugin normalisePlugin = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = tcPluginIO $ newIORef []- , tcPluginSolve = decideEqualSOP+ TcPlugin { tcPluginInit = return ()+ , tcPluginSolve = const decideEqualSOP , tcPluginStop = const (return ()) } -decideEqualSOP :: IORef [Ct] -> [Ct] -> [Ct] -> [Ct]+decideEqualSOP :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] [])-decideEqualSOP discharged givens _deriveds wanteds = do+decideEqualSOP _givens _deriveds [] = return (TcPluginOk [] [])+decideEqualSOP 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'@@ -115,61 +115,12 @@ sr <- simplifyNats (unit_givens ++ unit_wanteds) tcPluginTrace "normalised" (ppr sr) case sr of- Simplified _subst evs -> do- let solved = filter (isWanted . ctEvidence . (\(_,x,_) -> x)) evs- discharedWanteds <- tcPluginIO (readIORef discharged)- let existingWanteds = wanteds' ++ discharedWanteds- -- Create new wanted constraints- (solved',newWanteds) <- (second concat . unzip . catMaybes) <$>- mapM (evItemToCt existingWanteds) solved- -- update set of discharged wanteds- tcPluginIO (modifyIORef discharged (++ newWanteds))- -- return+ Simplified evs -> do+ let solved = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs+ (solved',newWanteds) = second concat (unzip solved) return (TcPluginOk solved' newWanteds) Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) -evItemToCt :: [Ct] -- ^ Existing wanteds- -> (EvTerm,Ct,CoreUnify CoreNote)- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-evItemToCt existingWanteds (ev,ct,subst)- | null newWanteds = return (Just ((ev,ct),[]))- | otherwise = do- newWanteds' <- catMaybes <$> mapM (substItemToCt existingWanteds) newWanteds- -- only allow new (conditional) evidence if conditional wanted constraints- -- can be added as new work- if length newWanteds == length newWanteds'- then return (Just ((ev,ct),newWanteds'))- else return Nothing- where- newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst--substItemToCt :: [Ct] -- ^ Existing wanteds wanted- -> UnifyItem TyVar CType CoreNote- -> TcPluginM (Maybe Ct)-substItemToCt existingWanteds si- | CType predicate `notElem` wantedPreds- , CType predicateS `notElem` wantedPreds- = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) (ctLoc ct))))- | otherwise- = return Nothing- where- predicate = unifyItemToPredType si- (ty1,ty2) = getEqPredTys predicate- predicateS = mkPrimEqPred ty2 ty1- ((ev,_,_),ct) = siNote si- wantedPreds = map (CType . ctPred) existingWanteds--unifyItemToPredType :: UnifyItem TyVar CType a -> 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- type NatEquality = (Ct,CoreSOP,CoreSOP) type NatInEquality = (Ct,CoreSOP) @@ -177,14 +128,12 @@ fromNatEquality (Left (ct, _, _)) = ct fromNatEquality (Right (ct, _)) = ct -type CoreNote = ((CoercionHole,TyVar,PredType), Ct)- data SimplifyResult- = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)]+ = Simplified [((EvTerm,Ct),[Ct])] | Impossible (Either NatEquality NatInEquality) instance Outputable SimplifyResult where- ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs+ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq simplifyNats :: [Either NatEquality NatInEquality]@@ -192,33 +141,35 @@ simplifyNats eqs = tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs where- simples :: CoreUnify CoreNote- -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)]+ simples :: [CoreUnify]+ -> [((EvTerm, Ct), [Ct])] -> [Either NatEquality NatInEquality] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult- simples subst evs _xs [] = return (Simplified subst (catMaybes evs))+ simples _subst evs _xs [] = return (Simplified evs) simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v) tcPluginTrace "unifyNats result" (ppr ur) case ur of- Win -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) []- (xs ++ eqs')- Lose -> return (Impossible eq)- Draw [] -> simples subst evs (eq:xs) eqs'+ Win -> do+ evs' <- maybe evs (:evs) <$> evMagic ct []+ simples subst 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 <*> pure subst''):evs)- [] (xs ++ eqs')- simples subst evs xs (eq@(Right (ct,u)):eqs') =- case isNatural u of- Just True -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) xs eqs'+ evM <- evMagic ct (map unifyItemToPredType subst')+ case evM of+ Nothing -> simples subst evs xs eqs'+ Just ev ->+ simples (substsSubst subst' subst ++ subst')+ (ev:evs) [] (xs ++ eqs')+ simples subst evs xs (eq@(Right (ct,u)):eqs') = do+ let u' = substsSOP subst u+ tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u'))+ case isNatural u' of+ Just True -> do+ evs' <- maybe evs (:evs) <$> evMagic ct []+ simples subst evs' xs eqs' Just False -> return (Impossible eq) Nothing -> simples subst evs (eq:xs) eqs' @@ -254,15 +205,33 @@ isNatKind :: Kind -> Bool isNatKind = (`eqType` typeNatKind) -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+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++evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))+evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 -> do+ holes <- replicateM (length preds) newCoercionHole+ let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes+ ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2+ 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+ natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)+ forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv+ let finalEv = foldl mkInstCo forallEv holeEvs+ return (Just ((EvCoercion finalEv, ct),newWanted))+ _ -> return Nothing++unifyItemToCt :: CtLoc+ -> PredType+ -> CoercionHole+ -> Ct+unifyItemToCt loc pred_type hole = mkNonCanonical (CtWanted pred_type (HoleDest hole) loc)
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -22,7 +22,6 @@ , reifySOP -- * Substitution on 'SOP' terms , UnifyItem (..)- , TyUnify , CoreUnify , substsSOP , substsSubst@@ -168,25 +167,21 @@ -- | 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 a = TyUnify TyVar CType a--type TyUnify v c n = [UnifyItem v c n]+type CoreUnify = UnifyItem TyVar CType -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- }+data UnifyItem v c = SubstItem { siVar :: v+ , siSOP :: SOP v c+ }+ | UnifyItem { siLHS :: SOP v c+ , siRHS :: SOP v c+ } -instance (Outputable v, Outputable c) => Outputable (UnifyItem v c n) where+instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) 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) => TyUnify v c n -> SOP v c -> SOP v c+substsSOP :: (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@@ -206,7 +201,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) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n+substsSubst :: (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}@@ -216,9 +211,9 @@ -- | 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 Ct) -- ^ Two terms are only equal if the given substitution holds+ = Win -- ^ Two terms are equal+ | Lose -- ^ Two terms are /not/ equal+ | Draw [CoreUnify] -- ^ Two terms are only equal if the given substitution holds instance Outputable UnifyResult where ppr Win = text "Win"@@ -241,11 +236,15 @@ then if containsConstants u || containsConstants v then if u == v then Win- else Draw (unifiers ct u v)+ else Draw (filter diffFromConstraint (unifiers ct u v)) else if u == v then Win else Lose- else Draw (unifiers ct u v)+ else Draw (filter diffFromConstraint (unifiers ct u v))+ where+ -- A unifier is only a unifier if differs from the original constraint+ diffFromConstraint (UnifyItem x y) = not (x == u && y == v)+ diffFromConstraint _ = True -- | Find unifiers for two SOP terms --@@ -280,38 +279,38 @@ -- @ -- [a := b] -- @-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct+unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] 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 ct]+ | 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 ct]+ | 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 ct]+ | 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 ct]+ | 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 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]+unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]+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 ct]-unifiers' ct s (S [P [V x]]) = [SubstItem x s ct]+unifiers' _ct (S [P [V x]]) s = [SubstItem x s]+unifiers' _ct s (S [P [V x]]) = [SubstItem x s] -unifiers' ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2 ct]-unifiers' ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]+unifiers' _ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2]+unifiers' _ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2] -- (z ^ a) ~ (z ^ b) ==> [a := b]@@ -400,11 +399,11 @@ | otherwise = ps2' psx = intersect ps1 ps2 -unifiers'' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct+unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify] unifiers'' ct (S [P [I i],P [V v]]) s2- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))] unifiers'' ct s1 (S [P [I i],P [V v]])- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))] unifiers'' _ _ _ = [] collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
tests/ErrorTests.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}+{-# LANGUAGE DataKinds, KindSignatures, TemplateHaskell, TypeFamilies, TypeOperators #-} {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}@@ -7,6 +7,10 @@ import Data.Proxy import GHC.TypeLits +import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)+import Language.Haskell.TH (litE, stringL)+import Language.Haskell.TH.Syntax (runIO)+ testProxy1 :: Proxy (x + 1) -> Proxy (2 + x) testProxy1 = id @@ -89,40 +93,69 @@ testProxy9 = proxyInEq testProxy9Errors =- ["Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"- ]+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"+ else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True"+ )] testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> () testProxy10 = proxyInEq' testProxy10Errors =- ["Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"- ]+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"+ else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False"+ )] testProxy11 :: Proxy (a :: Nat) -> Proxy a -> () testProxy11 = proxyInEq' testProxy11Errors =- ["Couldn't match type ‘'True’ with ‘'False’"- ]+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"+ else litE $ stringL "Couldn't match type 'True with 'False"+ )] testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> () testProxy12 = proxyInEq testProxy12Errors =- ["Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"- ]+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"+ else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True"+ )] testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->() testProxy13 = proxyInEq testProxy13Errors =- ["Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"- ]+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"+ else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True"+ )] testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> () testProxy14 = proxyInEq' testProxy14Errors =- ["Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"+ else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False"+ )]++type family CLog (b :: Nat) (x :: Nat) :: Nat+type instance CLog 2 2 = 1++testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)+testProxy15 = id++testProxy15Errors =+ ["Expected type: Proxy n -> Proxy (n + d)"+ ,"Actual type: Proxy n -> Proxy n" ]
tests/Tests.hs view
@@ -310,6 +310,7 @@ , 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+ , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $ (testProxy15 (Proxy :: Proxy 1)) `throws` testProxy15Errors , testGroup "Inequality" [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors