ghc-typelits-natnormalise 0.4.2 → 0.4.3
raw patch · 3 files changed
+47/−32 lines, 3 files
Files
- CHANGELOG.md +4/−0
- ghc-typelits-natnormalise.cabal +1/−1
- src/GHC/TypeLits/Normalise.hs +42/−31
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4.3 *July 18th 2016*+* Fixes bugs:+ * False positive: "f :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)"+ ## 0.4.2 *July 8th 2016* * Find more unifications: * `(2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]`
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.4.2+version: 0.4.3 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ of types of kind
src/GHC/TypeLits/Normalise.hs view
@@ -54,10 +54,14 @@ where -- external+import Control.Arrow (second) import Data.IORef (IORef, newIORef,readIORef, modifyIORef) import Data.List (intersect) import Data.Maybe (catMaybes, mapMaybe)-import GHC.TcPluginM.Extra (evByFiat, newGiven, tracePlugin)+import GHC.TcPluginM.Extra (tracePlugin)+#if __GLASGOW_HASKELL__ < 711+import GHC.TcPluginM.Extra (evByFiat)+#endif -- GHC API import Outputable (Outputable (..), (<+>), ($$), text)@@ -65,7 +69,7 @@ import TcEvidence (EvTerm (..)) import TcPluginM (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt) import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,- ctPred, ctLoc, isGiven, isWanted, mkNonCanonical)+ ctPred, isWanted, mkNonCanonical) import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, TyVar, classifyPredType, getEqPredTys, mkTyVarTy) import TysWiredIn (typeNatKind)@@ -74,7 +78,7 @@ import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo, mkNomReflCo, mkUnivCo) import TcPluginM (newCoercionHole, newFlexiTyVar)-import TcRnTypes (CtEvidence (..), TcEvDest (..))+import TcRnTypes (CtEvidence (..), TcEvDest (..), ctLoc) import TyCoRep (UnivCoProvenance (..)) import Type (mkPrimEqPred) import TcType (typeKind)@@ -126,45 +130,54 @@ sr <- simplifyNats (unit_givens ++ unit_wanteds) tcPluginTrace "normalised" (ppr sr) case sr of- Simplified subst evs -> do- let solved = filter (isWanted . ctEvidence . snd) evs- -- Create new wanted constraints-#if __GLASGOW_HASKELL__ >= 711- let newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst-#else- let newWanteds = filter (isWanted . ctEvidence . siNote) subst-#endif+ Simplified _subst evs -> do+ let solved = filter (isWanted . ctEvidence . (\(_,x,_) -> x)) evs discharedWanteds <- tcPluginIO (readIORef discharged) let existingWanteds = wanteds' ++ discharedWanteds- newWantedConstraints <- catMaybes <$>- mapM (substItemToCt existingWanteds)- newWanteds+ -- Create new wanted constraints+ (solved',newWanteds) <- (second concat . unzip . catMaybes) <$>+ mapM (evItemToCt existingWanteds) solved -- update set of discharged wanteds- tcPluginIO (modifyIORef discharged (++ newWantedConstraints))+ tcPluginIO (modifyIORef discharged (++ newWanteds)) -- return- return (TcPluginOk solved newWantedConstraints)+ return (TcPluginOk solved' newWanteds) #if __GLASGOW_HASKELL__ >= 711 Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) #else Impossible eq -> failWithProvenace (fromNatEquality eq) #endif +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+#if __GLASGOW_HASKELL__ >= 711+ newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst+#else+ newWanteds = filter (isWanted . ctEvidence . siNote) subst+#endif++ substItemToCt :: [Ct] -- ^ Existing wanteds wanted -> UnifyItem TyVar Type CoreNote -> TcPluginM (Maybe Ct) substItemToCt existingWanteds si- | isGiven (ctEvidence ct)- = Just <$> mkNonCanonical <$> newGiven loc predicate evTm-- -- Only create new wanteds | predicate `notElem` wantedPreds , predicateS `notElem` wantedPreds #if __GLASGOW_HASKELL__ >= 711- = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) loc)))+ = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) (ctLoc ct)))) #else = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate #endif- | otherwise = return Nothing where@@ -179,9 +192,6 @@ #endif wantedPreds = map ctPred existingWanteds - loc = ctLoc ct- evTm = evByFiat "ghc-typelits-natnormalise" ty1 ty2- unifyItemToPredType :: UnifyItem TyVar Type a -> PredType unifyItemToPredType ui = #if __GLASGOW_HASKELL__ >= 711@@ -209,7 +219,7 @@ #endif data SimplifyResult- = Simplified (CoreUnify CoreNote) [(EvTerm,Ct)]+ = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)] | Impossible NatEquality instance Outputable SimplifyResult where@@ -221,7 +231,7 @@ simplifyNats eqs = tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs where- simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct)] -> [NatEquality]+ simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)] -> [NatEquality] -> [NatEquality] -> TcPluginM SimplifyResult simples subst evs _xs [] = return (Simplified subst (catMaybes evs)) simples subst evs xs (eq@(ct,u,v):eqs') = do@@ -229,7 +239,7 @@ tcPluginTrace "unifyNats result" (ppr ur) case ur of #if __GLASGOW_HASKELL__ >= 711- Win -> simples subst (((,) <$> evMagic ct [] <*> pure ct):evs) []+ Win -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) [] (xs ++ eqs') Lose -> return (Impossible eq) Draw [] -> simples subst evs (eq:xs) eqs'@@ -241,17 +251,18 @@ let subst'' = zipWith (\si ev -> si {siNote = (ev,siNote si)}) subst' newEvs simples (substsSubst subst'' subst ++ subst'')- (((,) <$> evMagic ct newEvs <*> pure ct):evs)+ (((,,) <$> evMagic ct newEvs <*> pure ct <*> pure subst''):evs) [] (xs ++ eqs') #else- Win -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []+ Win -> simples subst (((,,) <$> evMagic ct <*> pure ct <*> pure []):evs) [] (xs ++ eqs') Lose -> return (Impossible eq) Draw [] -> simples subst evs (eq:xs) eqs' Draw subst' -> do simples (substsSubst subst' subst ++ subst')- (((,) <$> evMagic ct <*> pure ct):evs)+ (((,,) <$> evMagic ct <*> pure ct <*> pure subst'):evs) [] (xs ++ eqs')+ #endif -- Extract the Nat equality constraints