diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -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 diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -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 diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs --- a/src/GHC/TypeLits/Normalise/SOP.hs +++ b/src/GHC/TypeLits/Normalise/SOP.hs @@ -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 diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -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 diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -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"] diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -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