diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.8 *January 4th 2018* +* Add support for GHC 8.4.1-alpha1 + ## 0.5.7 *November 7th 2017* * Solve inequalities such as: `1 <= a + 3` diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ -Copyright (c) 2015-2016, University of Twente +Copyright (c) 2015-2016, University of Twente, + 2017-2018, QBayLogic B.V. All rights reserved. Redistribution and use in source and binary forms, with or without 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.5.7 +version: 0.5.8 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 @@ -42,12 +42,13 @@ author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com copyright: Copyright © 2015-2016, University of Twente, - 2017 , QBayLogic B.V. + 2017-2018, QBayLogic B.V. category: Type System build-type: Simple extra-source-files: README.md CHANGELOG.md cabal-version: >=1.10 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1 source-repository head type: git @@ -64,7 +65,7 @@ GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, - ghc >=8.0.1 && <8.4, + ghc >=8.0.1 && <8.6, ghc-tcplugins-extra >=0.2, integer-gmp >=1.0 && <1.1 hs-source-dirs: src 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 @@ -1,5 +1,6 @@ {-| -Copyright : (C) 2015-2016, University of Twente +Copyright : (C) 2015-2016, University of Twente, + 2017 , QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij @@ -53,8 +54,8 @@ import Control.Arrow (second) import Control.Monad (replicateM) import Data.Either (rights) -import Data.List (intersect) -import Data.Maybe (mapMaybe) +import Data.List (intersect, mapAccumR) +import Data.Maybe (catMaybes) import GHC.TcPluginM.Extra (tracePlugin) -- GHC API @@ -112,11 +113,11 @@ 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' + let unit_wanteds = catMaybes . snd $ mapAccumR toNatEquality [] wanteds' case unit_wanteds of [] -> return (TcPluginOk [] []) _ -> do - unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens + unit_givens <- catMaybes . snd . mapAccumR toNatEquality [] <$> mapM zonkCt givens sr <- simplifyNats unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr) case sr of @@ -147,56 +148,90 @@ -> [Either NatEquality NatInEquality] -- ^ Wanted constraints -> TcPluginM SimplifyResult -simplifyNats eqsG eqsW = - let eqs = eqsG ++ eqsW - in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs +simplifyNats givens wanteds = + let eqs = givens ++ wanteds + in tcPluginTrace "simplifyNats" (ppr eqs) >> + simples [] [] [] [] givens wanteds where - simples :: [CoreUnify] - -> [((EvTerm, Ct), [Ct])] - -> [Either NatEquality NatInEquality] - -> [Either NatEquality NatInEquality] - -> TcPluginM SimplifyResult - simples _subst evs _xs [] = return (Simplified evs) - simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do + simples + :: [CoreUnify] + -- Substitutions + -> [((EvTerm, Ct), [Ct])] + -- Evidence + -> [Either NatEquality NatInEquality] + -- Processed given constraints + -> [Either NatEquality NatInEquality] + -- Unsolved wanted constraints + -> [Either NatEquality NatInEquality] + -- Given constraints + -> [Either NatEquality NatInEquality] + -- Wanted constraints + -> TcPluginM SimplifyResult + -- Finished + simples _subst evs _eqGS _xs _eqG [] = return (Simplified evs) + -- Process all the givens (create substitutions) + simples subst evs eqGS xs (eq:eqs') ws + | Left (ct,u,v) <- eq = do ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v) - tcPluginTrace "unifyNats result" (ppr ur) case ur of + Lose -> return (Impossible eq) + Draw subst'@(_:_) -> do + evM <- evMagic ct (map unifyItemToPredType subst') + case evM of + Nothing -> simples subst evs eqGS xs eqs' ws + Just ev -> + simples (substsSubst subst' subst ++ subst') + (ev:evs) eqGS xs eqs' ws + _ -> simples subst evs eqGS xs eqs' ws + | Right (ct,u) <- eq = do + let u' = substsSOP subst u + case isNatural u' of + Just False -> return (Impossible eq) + -- Add a processed given with substitution applied + _ -> simples subst evs (Right (ct,u'):eqGS) xs eqs' ws + -- Process all the wanteds (actually solve constraints) + simples subst evs eqGS xs [] (eq:eqs') + | Left (ct,u,v) <- eq = do + ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v) + case ur of Win -> do evs' <- maybe evs (:evs) <$> evMagic ct [] - simples subst evs' [] (xs ++ eqs') + simples subst evs' eqGS [] [] (xs ++ eqs') Lose -> return (Impossible eq) - Draw [] -> simples subst evs (eq:xs) eqs' + Draw [] -> simples subst evs eqGS (eq:xs) [] eqs' Draw subst' -> do evM <- evMagic ct (map unifyItemToPredType subst') case evM of - Nothing -> simples subst evs xs eqs' + Nothing -> simples subst evs eqGS xs [] eqs' Just ev -> simples (substsSubst subst' subst ++ subst') - (ev:evs) [] (xs ++ eqs') - simples subst evs xs (eq@(Right (ct,u)):eqs') = do + (ev:evs) eqGS [] [] (xs ++ eqs') + | Right (ct,u) <- eq = 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' + simples subst evs' eqGS xs [] eqs' Just False -> return (Impossible 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. - if u `elem` (map snd (rights eqsG)) + if u' `elem` (map snd (rights eqGS)) then do evs' <- maybe evs (:evs) <$> evMagic ct [] - simples subst evs' xs eqs' - else simples subst evs (eq:xs) eqs' + simples subst evs' eqGS xs [] eqs' + else simples subst evs eqGS (eq:xs) [] eqs' -- Extract the Nat equality constraints -toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality) -toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of +toNatEquality + :: [(CType,Bool)] + -> Ct + -> ([(CType,Bool)],Maybe (Either NatEquality NatInEquality)) +toNatEquality a ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> go t1 t2 - _ -> Nothing + _ -> (a,Nothing) where go (TyConApp tc xs) (TyConApp tc' ys) | tc == tc' @@ -204,21 +239,40 @@ ,typeNatMulTyCon,typeNatExpTyCon]) = case filter (not . uncurry eqType) (zip xs ys) of [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y) - -> Just (Left (ct, normaliseNat x, normaliseNat y)) - _ -> Nothing + -> (a,Just (Left (ct, normaliseNat x, normaliseNat y))) + _ -> (a,Nothing) + + go (TyConApp tc xs) t2 | tc == typeNatLeqTyCon , [x,y] <- xs - = if tc' == promotedTrueDataCon - then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x]))) - else if tc' == promotedFalseDataCon - then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]]))) - else Nothing + = let trueLEq = (a,Just (Right (ct,normaliseNat + (mkTyConApp typeNatSubTyCon [y,x])))) + falseLEq = (a,Just (Right (ct,normaliseNat + (mkTyConApp typeNatSubTyCon + [x,mkTyConApp typeNatAddTyCon + [y,mkNumLitTy 1]])))) + in case t2 of + TyConApp tc' _ + | tc' == promotedTrueDataCon + -> trueLEq + | tc' == promotedFalseDataCon + -> falseLEq + _ | Just b <- lookup (CType t2) a + -> if b then trueLEq else falseLEq + | otherwise + -> (a,Nothing) + go x (TyConApp tc _) + | tc == promotedTrueDataCon + = ((CType x,True):a,Nothing) + | tc == promotedFalseDataCon + = ((CType x,False):a,Nothing) + go x y | isNatKind (typeKind x) && isNatKind (typeKind y) - = Just (Left (ct,normaliseNat x,normaliseNat y)) + = (a,Just (Left (ct,normaliseNat x,normaliseNat y))) | otherwise - = Nothing + = (a,Nothing) isNatKind :: Kind -> Bool isNatKind = (`eqType` typeNatKind) @@ -237,10 +291,18 @@ evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> do +#if MIN_VERSION_ghc(8,5,0) + holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) preds +#else holes <- replicateM (length preds) newCoercionHole +#endif let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2 +#if MIN_VERSION_ghc(8,5,0) + holeEvs = map mkHoleCo holes +#else holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds +#endif natReflCo = mkNomReflCo typeNatKind natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind) forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv 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 @@ -1,5 +1,6 @@ {-| -Copyright : (C) 2015-2016, University of Twente +Copyright : (C) 2015-2016, University of Twente, + 2017 , QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij -}