ghc-typelits-natnormalise 0.7 → 0.7.1
raw patch · 7 files changed
+619/−179 lines, 7 filesdep +sybdep ~ghcdep ~ghc-tcplugins-extraPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: syb
Dependency ranges changed: ghc, ghc-tcplugins-extra
API changes (from Hackage documentation)
+ GHC.TypeLits.Normalise.SOP: simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c
+ GHC.TypeLits.Normalise.Unify: normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
+ GHC.TypeLits.Normalise.Unify: normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type
+ GHC.TypeLits.Normalise.Unify: solvedInEqSmallestConstraint :: [(Bool, Set a)] -> (Bool, Set a)
- GHC.TypeLits.Normalise.Unify: instantSolveIneq :: Word -> Ineq -> Bool
+ GHC.TypeLits.Normalise.Unify: instantSolveIneq :: Word -> Ineq -> WriterT (Set CType) Maybe Bool
- GHC.TypeLits.Normalise.Unify: solveIneq :: Word -> Ineq -> Ineq -> Maybe Bool
+ GHC.TypeLits.Normalise.Unify: solveIneq :: Word -> Ineq -> Ineq -> WriterT (Set CType) Maybe Bool
Files
- CHANGELOG.md +6/−0
- ghc-typelits-natnormalise.cabal +5/−4
- src/GHC/TypeLits/Normalise.hs +316/−94
- src/GHC/TypeLits/Normalise/SOP.hs +2/−1
- src/GHC/TypeLits/Normalise/Unify.hs +126/−60
- tests/ErrorTests.hs +44/−4
- tests/Tests.hs +120/−16
CHANGELOG.md view
@@ -1,5 +1,11 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.7.1 *February 6th 2020*+* Add support for GHC 8.10.1-alpha2+* Fixes [#23](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/23): Can't figure out `+` commutes in some contexts on GHC 8.6.3+* Fixes [#28](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/28): Using the solver seems to break GHC+* Fixes [#34](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/34): inequality solver mishandles subtraction+ ## 0.7 *August 26th 2019* * Require KnownNat constraints when solving with constants
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.7+version: 0.7.1 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -49,7 +49,7 @@ 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.1+ GHC == 8.8.1, GHC == 8.10.1 source-repository head type: git@@ -67,9 +67,10 @@ GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.7,- ghc >=8.0.1 && <8.9,- ghc-tcplugins-extra >=0.3,+ ghc >=8.0.1 && <8.11,+ ghc-tcplugins-extra >=0.3.1, integer-gmp >=1.0 && <1.1,+ syb >=0.7.1 && <0.8, transformers >=0.5.2.0 && < 0.6 hs-source-dirs: src default-language: Haskell2010
src/GHC/TypeLits/Normalise.hs view
@@ -145,10 +145,10 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_HADDOCK show-extensions #-} @@ -158,16 +158,16 @@ -- external import Control.Arrow (second)-import Control.Monad ((<=<))+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 (rights)-import Data.List (intersect, stripPrefix)-import Data.Maybe (mapMaybe)-import Data.Set (Set, empty, toList)-import GHC.TcPluginM.Extra (tracePlugin)+import Data.Either (partitionEithers, rights)+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) import qualified GHC.TcPluginM.Extra as TcPluginM #if MIN_VERSION_ghc(8,4,0) import GHC.TcPluginM.Extra (flattenGivens)@@ -185,38 +185,78 @@ #endif import PrelNames (knownNatClassName) import TcEvidence (EvTerm (..))+#if MIN_VERSION_ghc(8,6,0)+import TcEvidence (evCast)+#endif #if !MIN_VERSION_ghc(8,4,0) import TcPluginM (zonkCt) #endif-import TcPluginM (TcPluginM, tcPluginTrace)-import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,- isWanted, mkNonCanonical)-import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType,- classifyPredType, eqType, getEqPredTys, mkTyVarTy)+import TcPluginM (TcPluginM, tcPluginTrace, tcPluginIO)+import Type (Kind, PredType, eqType, mkTyVarTy) import TysWiredIn (typeNatKind) -import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,- mkNomReflCo, mkUnivCo)-import TcPluginM (newCoercionHole, newFlexiTyVar, tcLookupClass)-import TcRnTypes- (CtEvidence (..), CtLoc, TcEvDest (..), ctEvLoc, ctLoc, ctLocSpan, isGiven,- setCtLoc, setCtLocSpan)-#if MIN_VERSION_ghc(8,2,0)-import TcRnTypes (ShadowInfo (WDeriv))-#endif+import Coercion (CoercionHole, Role (..), mkUnivCo)+import TcPluginM (newCoercionHole, tcLookupClass)+import TcRnTypes (TcPlugin (..), TcPluginResult(..)) import TyCoRep (UnivCoProvenance (..))-import Type (mkClassPred, mkPrimEqPred)-import TcType (typeKind)+import TcType (isEqPred) import TyCoRep (Type (..)) import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) import TcTypeNats (typeNatLeqTyCon) import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)+import Data.IORef +#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)+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, getEqPredTys, mkClassPred,+ mkPrimEqPred)+#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+ -- internal+import GHC.TypeLits.Normalise.SOP import GHC.TypeLits.Normalise.Unify +#if !MIN_VERSION_ghc(8,10,0)+isEqPrimPred :: PredType -> Bool+isEqPrimPred = isEqPred+#endif+ -- | To use the plugin, add -- -- @@@ -242,46 +282,169 @@ normalisePlugin :: Opts -> TcPlugin normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = return ()- , tcPluginSolve = const (decideEqualSOP opts)+ TcPlugin { tcPluginInit = tcPluginIO $ newIORef empty+ , tcPluginSolve = decideEqualSOP opts , tcPluginStop = const (return ()) }+newtype OrigCt = OrigCt { runOrigCt :: Ct } decideEqualSOP :: Opts+ -> IORef (Set CType)+ -- ^ Givens that is already generated.+ -- We have to generate new givens at most once;+ -- otherwise GHC will loop indefinitely. -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult-decideEqualSOP _opts _givens _deriveds [] = return (TcPluginOk [] [])-decideEqualSOP opts givens _deriveds wanteds = do++-- 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 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 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 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'- case unit_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do #if MIN_VERSION_ghc(8,4,0)- let unit_givens = mapMaybe toNatEquality (givens ++ flattenGivens givens)+ let simplGivens = givens ++ flattenGivens givens+ subst = fst $ unzip $ TcPluginM.mkSubst' givens+ wanteds0 = map (\ct -> (OrigCt ct,+ TcPluginM.substCt subst ct+ )+ ) wanteds #else- unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens+ let wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds+ simplGivens <- mapM zonkCt givens #endif+ let wanteds' = filter (isWanted . ctEvidence) wanteds+ unit_wanteds = mapMaybe toNatEquality wanteds'+ nonEqs = filter (not . (\p -> isEqPred p || isEqPrimPred p) . ctEvPred . ctEvidence.snd)+ $ filter (isWanted. ctEvidence.snd) wanteds0+ done <- tcPluginIO $ readIORef gen'd+ let redGs = reduceGivens opts 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 simplGivens sr <- simplifyNats opts unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr)+ reds <- forM reducible_wanteds $ \(origCt,(term, ws)) -> do+ wants <- evSubtPreds origCt $ subToPred opts ws+ return ((term, origCt), wants) case sr of Simplified evs -> do- let solved = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs- (solved',newWanteds) = second concat (unzip solved)- return (TcPluginOk solved' newWanteds)+ let simpld = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs+ (solved',newWanteds) = second concat (unzip $ simpld ++ 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 -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]+reduceGivens opts done givens =+ let nonEqs =+ [ ct+ | ct <- givens+ , let ev = ctEvidence ct+ prd = ctEvPred ev+ , isGiven ev+ , not $ (\p -> isEqPred p || isEqPrimPred p) prd+ ]+ in filter+ (\(_, (prd, _, _)) ->+ notMember (CType prd) done+ )+ $ mapMaybe+ (\ct -> (ct,) <$> tryReduceGiven opts givens ct)+ nonEqs++tryReduceGiven+ :: Opts -> [Ct] -> Ct+ -> Maybe (PredType, EvTerm, [PredType])+tryReduceGiven opts simplGivens ct = do+ let (mans, ws) =+ runWriter $ normaliseNatEverywhere $+ ctEvPred $ ctEvidence ct+ ws' = [ p+ | (p, _) <- subToPred opts 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)]))+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+ Nothing -> return Nothing+ 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)@@ -298,16 +461,24 @@ -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Wanted constraints -> TcPluginM SimplifyResult-simplifyNats (Opts {..}) eqsG eqsW =- let eqs = map (second (const [])) eqsG ++ eqsW- in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] [] eqs+simplifyNats opts@Opts {..} 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)+ foldr findFirstSimpliedWanted (Simplified []) <$>+ mapM (\v -> do let eqs = v ++ eqsW+ tcPluginTrace "simplifyNats" (ppr eqs)+ simples [] [] [] [] eqs)+ fancyGivens where- -- 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 | negNumbers = const []- | otherwise = map subtractionToPred- simples :: [CoreUnify] -> [((EvTerm, Ct), [Ct])] -> [(CoreSOP,CoreSOP,Bool)]@@ -322,7 +493,7 @@ tcPluginTrace "unifyNats result" (ppr ur) case ur of Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred k)+ evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts k) simples subst evs' leqsG [] (xs ++ eqs') Lose -> if null evs && null eqs' then return (Impossible (fst eq))@@ -330,7 +501,7 @@ Draw [] -> simples subst evs [] (eq:xs) eqs' Draw subst' -> do evM <- evMagic ct empty (map unifyItemToPredType subst' ++- subToPred k)+ subToPred opts k) let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG | otherwise = leqsG case evM of@@ -352,29 +523,86 @@ 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 k)+ evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts k) simples subst evs' leqsG' xs eqs' - Just (False,_) -> return (Impossible (fst eq))- Nothing- -- 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 (mapMaybe (solveIneq depth u) ineqs) ||- -- Or the above, but with valid substitutions applied to the wanted.- or (mapMaybe (solveIneq depth uS) ineqs) ||- -- Or it is an inequality that can be instantly solved, such as- -- `1 <= x^y`- instantSolveIneq depth u- -> do- evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred k)- simples subst evs' leqsG' xs eqs'- | otherwise- -> simples subst evs leqsG (eq: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:+ -- 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 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 -> [(Type, Type)] -> [(PredType, Kind)]+subToPred Opts{..}+ | negNumbers = const []+ | otherwise = map subtractionToPred+ -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)]) toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of@@ -429,37 +657,36 @@ SubstItem {..} -> reifySOP siSOP UnifyItem {..} -> reifySOP siRHS -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- let predTypes = map fst preds- predKinds = map snd preds+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+ holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes #else- holes <- replicateM (length preds) newCoercionHole+ 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 newWanted = knWanted ++ zipWith (unifyItemToCt (ctLoc ct)) predTypes holes- ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2-#if MIN_VERSION_ghc(8,4,1)- holeEvs = map mkHoleCo holes-#else- holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes predTypes-#endif- forallEv <- mkForAllCos <$> (mapM mkCoVar predKinds) <*> pure ctEv- let finalEv = foldl mkInstCo forallEv holeEvs+ let newWant = knWanted ++ holeWanteds+ ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2 #if MIN_VERSION_ghc(8,5,0)- return (Just ((EvExpr (Coercion finalEv), ct),newWanted))+ return (Just ((EvExpr (Coercion ctEv), ct),newWant)) #else- return (Just ((EvCoercion finalEv, ct),newWanted))+ return (Just ((EvCoercion ctEv, ct),newWant)) #endif _ -> return Nothing- where- mkCoVar k = (,natReflCo) <$> (newFlexiTyVar k)- where- natReflCo = mkNomReflCo k +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@@ -468,12 +695,7 @@ kc_clas <- tcLookupClass knownNatClassName let kn_pred = mkClassPred kc_clas [ty] wantedCtEv <- TcPluginM.newWanted (ctLoc ct) kn_pred- let wanted = mkNonCanonical wantedCtEv- -- Set the source-location of the new wanted constraint to the source- -- location of the [W]anted constraint we are currently trying to solve- ct_ls = ctLocSpan (ctLoc ct)- ctl = ctEvLoc wantedCtEv- wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)+ let wanted' = mkNonCanonical' (ctLoc ct) wantedCtEv return wanted' unifyItemToCt :: CtLoc
src/GHC/TypeLits/Normalise/SOP.hs view
@@ -85,6 +85,7 @@ , mergeSOPAdd , mergeSOPMul , normaliseExp+ , simplifySOP ) where @@ -275,7 +276,7 @@ normaliseExp b@(S [P [_]]) (S [e@(P [_])]) = S [P [reduceExp (E b e)]] -- (x + 2)^2 ==> x^2 + 4xy + 4-normaliseExp b (S [P [(I i)]]) =+normaliseExp b (S [P [(I i)]]) | i > 0 = foldr1 mergeSOPMul (replicate (fromInteger i) b) -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -20,6 +20,8 @@ CType (..) , CoreSOP , normaliseNat+ , normaliseNatEverywhere+ , normaliseSimplifyNat , reifySOP -- * Substitution on 'SOP' terms , UnifyItem (..)@@ -38,19 +40,21 @@ , ineqToSubst , subtractionToPred , instantSolveIneq+ , solvedInEqSmallestConstraint -- * Properties , isNatural ) where -- External-import Control.Arrow (second)+import Control.Arrow (first, second) import Control.Monad.Trans.Maybe import Control.Monad.Trans.Writer.Strict import Data.Function (on) import Data.List ((\\), intersect, mapAccumL, nub) import Data.Maybe (fromMaybe, mapMaybe) import Data.Set (Set)+import Data.Generics (mkM, everywhereM) import qualified Data.Set as Set import GHC.Base (isTrue#,(==#))@@ -60,18 +64,25 @@ -- GHC API import Outputable (Outputable (..), (<+>), ($$), text) import TcPluginM (TcPluginM, tcPluginTrace)-import TcRnMonad (Ct, ctEvidence, isGiven)-import TcRnTypes (ctEvPred) import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatLeqTyCon)-import Type (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,+import Type (TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,- nonDetCmpType, PredType, mkPrimEqPred)+ nonDetCmpType, PredType, typeKind) import TyCoRep (Kind, Type (..), TyLit (..))-import TysWiredIn (boolTy, promotedTrueDataCon)+import TysWiredIn (boolTy, promotedTrueDataCon, typeNatKind) import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet) +#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+ -- Internal import GHC.TypeLits.Normalise.SOP @@ -112,6 +123,27 @@ | tc == typeNatExpTyCon = normaliseExp <$> normaliseNat x <*> normaliseNat y normaliseNat t = return (S [P [C (CType t)]]) +-- | Applies 'normaliseNat' and 'simplifySOP' to type or predicats+-- to reduce any occurence 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 ty+ | typeKind ty `eqType` typeNatKind = do+ ty' <- normaliseSimplifyNat ty+ return $ if ty `eqType` ty' then Nothing else Just ty'+ | otherwise = do+ ty' <- everywhereM (mkM normaliseSimplifyNat) ty+ return $ if ty `eqType` ty' then Nothing else Just ty'++normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type+normaliseSimplifyNat ty+ | typeKind ty `eqType` typeNatKind = do+ ty' <- normaliseNat ty+ return $ reifySOP $ simplifySOP ty'+ | otherwise = return ty+ -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type reifySOP = combineP . map negateP . unS@@ -238,11 +270,11 @@ -- made, for use when turning the substitution back into constraints. type CoreUnify = UnifyItem TyVar CType -data UnifyItem v c = SubstItem { siVar :: v- , siSOP :: SOP v c+data UnifyItem v c = SubstItem { siVar :: v+ , siSOP :: SOP v c }- | UnifyItem { siLHS :: SOP v c- , siRHS :: SOP v c+ | UnifyItem { siLHS :: SOP v c+ , siRHS :: SOP v c } deriving Eq @@ -427,13 +459,13 @@ -- 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]])- _ -> []+ Just k -> 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]])- _ -> []+ Just k -> 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)])@@ -466,9 +498,9 @@ _ | 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)+ [] -> unifiers'' ct (S ps1) (S ps2) [k] | length ps1 == length ps2 -> [k]- _ -> []+ _ -> [] | null psx , isGiven (ctEvidence ct) -> unifiers'' ct (S ps1) (S ps2)@@ -581,7 +613,7 @@ -- ^ Inequality we want to solve -> Ineq -- ^ Given/proven inequality- -> Maybe Bool+ -> WriterT (Set CType) Maybe Bool -- ^ Solver result -- -- * /Nothing/: exhausted solver steps@@ -590,19 +622,46 @@ -- -- * /Just False/: solver is unable to solve inequality, note that this does -- __not__ mean the wanted inequality does not hold.-solveIneq 0 _ _ = Nothing+solveIneq 0 _ _ = noRewrite solveIneq k want@(_,_,True) have@(_,_,True) | want == have- = Just True- | null solved- = Nothing+ = pure True | otherwise- = Just (or solved)- where- solved = mapMaybe (uncurry (solveIneq (k - 1))) new- new = concatMap (\f -> f want have) ineqRules-solveIneq _ _ _ = Just False+ = do+ let -- Apply all the rules, and get all the successful ones+ new = mapMaybe (\f -> runWriterT (f want have)) ineqRules+ -- Recurse down with all the transformed equations+ solved = map (first (mapMaybe (runWriterT . uncurry (solveIneq (k-1))))) new+ -- For the results of every recursive call, find the one that yields+ -- 'True' and has the smallest set of constraints.+ solved1 = map (first solvedInEqSmallestConstraint) solved+ -- Union the constraints from the corresponding rewrites with the+ -- constraints from the recursive results+ solved2 = map (\((b,s1),s2) -> (b,Set.union s1 s2)) solved1+ -- From these results, again find the single result that yields 'True'+ -- and has the smallest set of constraints.+ solved3 = solvedInEqSmallestConstraint solved2+ if null solved then+ noRewrite+ else do+ WriterT (Just solved3) +solveIneq _ _ _ = pure False++-- Find the solved inequality with the fewest number of constraints+solvedInEqSmallestConstraint :: [(Bool,Set a)] -> (Bool, Set a)+solvedInEqSmallestConstraint = go (False, Set.empty)+ where+ go bs [] = bs+ go (b,s) ((b1,s1):solved)+ | not b && b1+ = go (b1,s1) solved+ | b && b1+ , Set.size s > Set.size s1+ = go (b1,s1) solved+ | otherwise+ = go (b,s) solved+ -- | Try to instantly solve an inequality by using the inequality solver using -- @1 <=? 1 ~ True@ as the given constraint. instantSolveIneq@@ -610,16 +669,17 @@ -- ^ Solving depth -> Ineq -- ^ Inequality we want to solve- -> Bool-instantSolveIneq k u = case solveIneq k u (one,one,True) of- Just p -> p- Nothing -> False+ -> WriterT (Set CType) Maybe Bool+instantSolveIneq k u = solveIneq k u (one,one,True) where one = S [P [I 1]] type Ineq = (CoreSOP, CoreSOP, Bool)-type IneqRule = Ineq -> Ineq -> [(Ineq,Ineq)]+type IneqRule = Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq,Ineq)] +noRewrite :: WriterT (Set CType) Maybe a+noRewrite = WriterT Nothing+ ineqRules :: [IneqRule] ineqRules =@@ -643,7 +703,7 @@ | S [P [I a']] <- a , S [P [I x']] <- x , x' >= a'- = [(want,(a,y,le))]+ = pure [(want,(a,y,le))] -- want: y <=? 10 ~ True -- have: y <=? 9 ~ True --@@ -652,8 +712,8 @@ | S [P [I b']] <- b , S [P [I y']] <- y , y' < b'- = [(want,(x,b,le))]-leTrans _ _ = []+ = pure [(want,(x,b,le))]+leTrans _ _ = noRewrite -- | Monotonicity of addition --@@ -667,27 +727,27 @@ plusMonotone want have | Just want' <- sopToIneq (subtractIneq want) , want' /= want- = [(want',have)]+ = pure [(want',have)] | Just have' <- sopToIneq (subtractIneq have) , have' /= have- = [(want,have')]-plusMonotone _ _ = []+ = pure [(want,have')]+plusMonotone _ _ = noRewrite -- | Make the `a` of a given `a <= b` smaller haveSmaller :: IneqRule haveSmaller want have | (S (x:y:ys),us,True) <- have- = [(want,(S (x:ys),us,True))+ = pure [(want,(S (x:ys),us,True)) ,(want,(S (y:ys),us,True)) ] | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have- = [(want,(S [P [I 1]],S [P p],True))]-haveSmaller _ _ = []+ = pure [(want,(S [P [I 1]],S [P p],True))]+haveSmaller _ _ = noRewrite -- | Make the `b` of a given `a <= b` bigger haveBigger :: IneqRule haveBigger want have- | (_,S vs,True) <- want+ | (_ ,S vs,True) <- want , (as,S bs,True) <- have , let vs' = vs \\ bs , not (null vs')@@ -696,8 +756,14 @@ -- -- new want: want -- new have: y <= x + 1- = [(want,(as,mergeSOPAdd (S bs) (S vs'),True))]-haveBigger _ _ = []+ = do+ -- Ensure that we're actually making the RHS larger+ b <- isNatural (S vs')+ if b then+ pure [(want,(as,mergeSOPAdd (S bs) (S vs'),True))]+ else+ noRewrite+haveBigger _ _ = noRewrite -- | Monotonicity of multiplication timesMonotone :: IneqRule@@ -717,7 +783,7 @@ , not (null ay) -- Pick the smallest product , let az = if length ax <= length ay then S [P ax] else S [P ay]- = [(want,(mergeSOPMul az x, mergeSOPMul az y,le))]+ = pure [(want,(mergeSOPMul az x, mergeSOPMul az y,le))] -- want: a <=? C*b ~ True -- have: x <=? y ~ True@@ -734,7 +800,7 @@ , not (null by) -- Pick the smallest product , let bz = if length bx <= length by then S [P bx] else S [P by]- = [(want,(mergeSOPMul bz x, mergeSOPMul bz y,le))]+ = pure [(want,(mergeSOPMul bz x, mergeSOPMul bz y,le))] -- want: a <=? b ~ True -- have: C*x <=? y ~ True@@ -751,7 +817,7 @@ , not (null xb) -- Pick the smallest product , let xz = if length xa <= length xb then S [P xa] else S [P xb]- = [((mergeSOPMul xz a, mergeSOPMul xz b,le),have)]+ = pure [((mergeSOPMul xz a, mergeSOPMul xz b,le),have)] -- want: a <=? b ~ True -- have: x <=? C*y ~ True@@ -768,9 +834,9 @@ , not (null yb) -- Pick the smallest product , let yz = if length ya <= length yb then S [P ya] else S [P yb]- = [((mergeSOPMul yz a, mergeSOPMul yz b,le),have)]+ = pure [((mergeSOPMul yz a, mergeSOPMul yz b,le),have)] -timesMonotone _ _ = []+timesMonotone _ _ = noRewrite -- | Monotonicity of exponentiation powMonotone :: IneqRule@@ -783,22 +849,22 @@ -- new want: want -- new have: x <=? y ~ True | xS == yS- -> [(want,(S [xP],S [yP],le))]+ -> pure [(want,(S [xP],S [yP],le))] -- want: XXX -- have: x^2 <=? y^2 ~ True -- -- new want: want -- new have: x <=? y ~ True | xP == yP- -> [(want,(xS,yS,le))]+ -> pure [(want,(xS,yS,le))] -- want: XXX -- have: 2 <=? 2 ^ x ~ True -- -- new want: want -- new have: 1 <=? x ~ True _ | x == yS- -> [(want,(S [P [I 1]],S [yP],le))]- _ -> []+ -> pure [(want,(S [P [I 1]],S [yP],le))]+ _ -> noRewrite powMonotone (a,S [P [E bS bP]],le) have = case a of@@ -809,24 +875,24 @@ -- new want: x <=? y ~ True -- new have: have | aS == bS- -> [((S [aP],S [bP],le),have)]+ -> pure [((S [aP],S [bP],le),have)] -- want: x^2 <=? y^2 ~ True -- have: XXX -- -- new want: x <=? y ~ True -- new have: have | aP == bP- -> [((aS,bS,le),have)]+ -> pure [((aS,bS,le),have)] -- want: 2 <=? 2 ^ x ~ True -- have: XXX -- -- new want: 1 <=? x ~ True -- new have: XXX _ | a == bS- -> [((S [P [I 1]],S [bP],le),have)]- _ -> []+ -> pure [((S [P [I 1]],S [bP],le),have)]+ _ -> noRewrite -powMonotone _ _ = []+powMonotone _ _ = noRewrite -- | Try to get the power-of-2 factors, and apply the monotonicity of -- exponentiation rule.@@ -844,7 +910,7 @@ -- new have: have | Just a' <- facSOP 2 a , Just b' <- facSOP 2 b- = [((a',b',le),have)]+ = pure [((a',b',le),have)] pow2MonotoneSpecial want (x,y,le) -- want: XXX -- have:4 * 4^x <=? 8^x ~ True@@ -855,8 +921,8 @@ -- new have: 2+2*x <=? 3*x ~ True | Just x' <- facSOP 2 x , Just y' <- facSOP 2 y- = [(want,(x',y',le))]-pow2MonotoneSpecial _ _ = []+ = pure [(want,(x',y',le))]+pow2MonotoneSpecial _ _ = noRewrite -- | Get the power of /N/ factors of a SOP term facSOP
tests/ErrorTests.hs view
@@ -1,9 +1,17 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} #if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE NoStarIsType #-} #endif {-# OPTIONS_GHC -fdefer-type-errors #-}@@ -181,3 +189,35 @@ then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’" else litE $ stringL "Couldn't match type `1 <=? n' with 'True" )]++data Dict c where+ Dict :: c => Dict c+deriving instance Show (Dict c)+data Boo (n :: Nat) = Boo++test17 :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String+test17 = const show++testProxy17 :: String++testProxy17 = test17 (Proxy :: Proxy 17) Boo+test17Errors =+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’"+ else litE $ stringL "Couldn't match type `1 <=? n' with 'True"+ )]++test19f :: (1 <= n)+ => Proxy n -> Proxy n+test19f = id++testProxy19 :: (1 <= m, m <= rp)+ => Proxy m+ -> Proxy rp+ -> Proxy (rp - m)+ -> Proxy (rp - m)+testProxy19 _ _ = test19f++test19Errors =+ ["Could not deduce: (1 <=? (rp - m)) ~ 'True"]
tests/Tests.hs view
@@ -1,20 +1,26 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE NoImplicitPrelude #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} #if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE NoStarIsType #-} #endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -dcore-lint #-} import GHC.TypeLits import Unsafe.Coerce@@ -129,7 +135,7 @@ -- >>> init (1:>2:>3:>Nil) -- <1,2> init :: Vec (n + 1) a -> Vec n a-init (_ :> Nil) = Nil+init (_ :> Nil) = Nil init (x :> y :> ys) = x :> init (y :> ys) init' :: (1 <= m) => Vec m a -> Vec (m-1) a@@ -268,12 +274,12 @@ at' = at @m @(k - 1 - m) leToPlus- :: forall (k :: Nat) (n :: Nat) f r+ :: forall (k :: Nat) (n :: Nat) (f :: Nat -> Type) (r :: Type) . (k <= n) => Proxy k -> f n -- ^ Argument with the @(k <= n)@ constraint- -> (forall m . f (m + k) -> r)+ -> (forall (m :: Nat) . f (m + k) -> r) -- ^ Function with the @(n + k)@ constraint -> r leToPlus _ a f = f @ (n-k) a@@ -401,6 +407,38 @@ succAtMost :: AtMost n -> AtMost (n + 1) succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a) +eqReduceForward+ :: Eq (Boo (n + 1))+ => Dict (Eq (Boo (n + 2 - 1)))+eqReduceForward = Dict++eqReduceForwardMinusPlus+ :: (Eq (Boo (0 + n + 1)), 1 <= n)+ => Dict (Eq (Boo (n - 1 + 2)))+eqReduceForwardMinusPlus = Dict++eqReduceBackward+ :: (Eq (Boo (m + 2 - 1)))+ => Dict (Eq (Boo (m + 1)))+eqReduceBackward = Dict++eqReduceBackward'+ :: (Eq (Boo (1 + m + 2)))+ => Dict (Eq (Boo (m + 3)))+eqReduceBackward' = Dict++proxyInEq8fun+ :: (1 <= (n + CLog 2 n))+ => Proxy n+ -> Proxy n+proxyInEq8fun = id++proxyInEq8+ :: (1 <= n, KnownNat (CLog 2 n))+ => Proxy n+ -> Proxy n+proxyInEq8 = proxyInEq8fun+ main :: IO () main = defaultMain tests @@ -495,6 +533,9 @@ , testCase "1 <= G a implies F a <= G a * F a" $ show (proxyInEqImplication4 (Proxy :: Proxy 2)) @?= "Proxy"+ , testCase "`(1 <= n)` only implies `(1 <= n + F n)` when `KnownNat (F n)`" $+ show (proxyInEq8 (Proxy :: Proxy 2)) @?=+ "Proxy" ] , testGroup "errors" [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors@@ -504,7 +545,8 @@ , 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+ , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $+ testProxy15 (Proxy :: Proxy 1) `throws` testProxy15Errors , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors , testGroup "Inequality" [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors@@ -513,6 +555,9 @@ , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors+ , testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $+ testProxy17 `throws` test17Errors+ , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @ 1) (Proxy @ 1)) `throws` test19Errors ] ] ]@@ -529,3 +574,62 @@ if all (`isInfixOf` msg) xs then return () else assertFailure msg++showFin :: forall n. KnownNat n => Fin n -> String+showFin f = mconcat [+ show (finToInt f)+ , "/"+ , show (natVal (Proxy :: Proxy n))+ ]++finToInt :: Fin n -> Int+finToInt FZ = 0+finToInt (FS fn) = finToInt fn + 1++predFin :: Fin (n + 2) -> Fin (n + 1)+predFin (FS fn) = fn+predFin FZ = FZ++showSucPred :: KnownNat (n + 2) => Fin (n + 2) -> String+showSucPred = showFin . FS . predFin++class Up env (n :: Nat) where+ up :: env -> Fin n -> Fin (n + 1)++class Down env (n :: Nat) where+ down :: env -> Fin n -> Fin (n - 1)++class ShowWith env (n :: Nat) where+ showWith :: env -> Fin n -> String++showDownUp+ :: (Up env n, Down env (n + 1), ShowWith env n)+ => env -> Fin n -> String+showDownUp env fn = showWith env $ down env $ up env fn++showDownUp'+ :: (Up env n, Down env (n + 1), KnownNat n)+ => env -> Fin n -> String+showDownUp' env fn = showFin $ down env $ up env fn++data family FakeUVector (n :: Nat) :: Type+data family FakeMUVector (n :: Nat) :: Type+type family Mutable (v :: Nat -> Type) :: Nat -> Type+type instance Mutable FakeUVector = FakeMUVector++class (IsMVector FakeMUVector n, IsVector FakeUVector n)+ => FakeUnbox n+class IsMVector (v :: Nat -> Type) a where+ touchMVector :: v a -> v a+class IsMVector (Mutable v) a => IsVector v a where+ touchVector :: v a -> v a++newtype WrapFakeVector n = WFV { unWrap :: FakeUVector (1 + n) }+newtype WrapFakeMVector n = MWFV { unWrapM :: FakeMUVector (1 + n) }+type instance Mutable WrapFakeVector = WrapFakeMVector++-- The following two instances cannot be derived without simplification phase!+instance FakeUnbox (n + 1) => IsVector WrapFakeVector n where+ touchVector = WFV . touchVector . unWrap+instance FakeUnbox (n + 1) => IsMVector WrapFakeMVector n where+ touchMVector = MWFV . touchMVector . unWrapM