th-abstraction 0.2.7.0 → 0.2.8.0
raw patch · 6 files changed
+407/−46 lines, 6 filesdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: template-haskell
API changes (from Hackage documentation)
Files
- ChangeLog.md +19/−0
- src/Language/Haskell/TH/Datatype.hs +190/−33
- test/Harness.hs +26/−2
- test/Main.hs +143/−6
- test/Types.hs +28/−4
- th-abstraction.cabal +1/−1
ChangeLog.md view
@@ -1,5 +1,24 @@ # Revision history for th-abstraction +## 0.2.8.0 -- 2018-06-29+* GADT reification is now much more robust with respect to `PolyKinds`:+ * A bug in which universally quantified kind variables were mistakenly+ flagged as existential has been fixed.+ * A bug in which the kinds of existentially quantified type variables+ were not substituted properly has been fixed.+ * More kind equalities are detected than before. For example, in the+ following data type:++ ```haskell+ data T (a :: k) where+ MkT :: forall (a :: Bool). T a+ ```++ We now catch the `k ~ Bool` equality.+* Tweak `resolveTypeSynonyms` so that failing to reify a type constructor+ name so longer results in an error. Among other benefits, this makes+ it possible to pass data types with GADT syntax to `normalizeDec`.+ ## 0.2.7.0 -- 2018-06-17 * Fix bug in which data family instances with duplicate occurrences of type variables in the left-hand side would have redundant equality constraints
src/Language/Haskell/TH/Datatype.hs view
@@ -776,16 +776,9 @@ -> ConstructorVariant -> Q [ConstructorInfo] dataFamCase' n tyvars stricts variant = do- info <- reifyRecover n $ fail $ unlines- [ "normalizeCon: Cannot reify constructor " ++ nameBase n- , "You are likely calling normalizeDec on GHC 7.6 or 7.8 on a data family"- , "whose type variables have been eta-reduced due to GHC Trac #9692."- , "Unfortunately, without being able to reify the constructor's type,"- , "there is no way to recover the eta-reduced type variables in general."- , "A recommended workaround is to use reifyDatatype instead."- ]- case info of- DataConI _ ty _ _ -> do+ mbInfo <- reifyMaybe n+ case mbInfo of+ Just (DataConI _ ty _ _) -> do let (context, argTys :|- returnTy) = uncurryType ty returnTy' <- resolveTypeSynonyms returnTy -- Notice that we've ignored the Cxt and argument Types from the@@ -800,7 +793,14 @@ -- much easier. normalizeGadtC typename params tyvars context [n] returnTy' argTys stricts (const $ return variant)- _ -> fail "normalizeCon: impossible"+ _ -> fail $ unlines+ [ "normalizeCon: Cannot reify constructor " ++ nameBase n+ , "You are likely calling normalizeDec on GHC 7.6 or 7.8 on a data family"+ , "whose type variables have been eta-reduced due to GHC Trac #9692."+ , "Unfortunately, without being able to reify the constructor's type,"+ , "there is no way to recover the eta-reduced type variables in general."+ , "A recommended workaround is to use reifyDatatype instead."+ ] -- A very ad hoc way of determining if we need to perform some extra passes -- to repair an eta-reduction bug for data family instances that only occurs@@ -909,13 +909,17 @@ case decomposeType innerType' of ConT innerTyCon :| ts | typename == innerTyCon -> - let (substName, context1) = mergeArguments params ts- subst = VarT <$> substName- tyvars' = [ tv | tv <- renamedTyvars, Map.notMember (tvName tv) subst ]+ let (substName, context1) =+ closeOverKinds (kindsOfFVsOfTvbs renamedTyvars)+ (kindsOfFVsOfTypes params)+ (mergeArguments params ts)+ subst = VarT <$> substName+ exTyvars = [ tv | tv <- renamedTyvars, Map.notMember (tvName tv) subst ] - context2 = applySubstitution subst (context1 ++ renamedContext)- fields' = applySubstitution subst renamedFields- in sequence [ ConstructorInfo name tyvars' context2+ exTyvars' = substTyVarBndrs subst exTyvars+ context2 = applySubstitution subst (context1 ++ renamedContext)+ fields' = applySubstitution subst renamedFields+ in sequence [ ConstructorInfo name exTyvars' context2 fields' stricts <$> variantQ | name <- names , let variantQ = getVariant name@@ -923,6 +927,120 @@ _ -> fail "normalizeGadtC: Expected type constructor application" +{-+Extend a type variable renaming subtitution and a list of equality+predicates by looking into kind information as much as possible.++Why is this necessary? Consider the following example:++ data (a1 :: k1) :~: (b1 :: k1) where+ Refl :: forall k2 (a2 :: k2). a2 :~: a2++After an initial call to mergeArguments, we will have the following+substitution and context:++* Substitution: [a2 :-> a1]+* Context: (a2 ~ b1)++We shouldn't stop there, however! We determine the existentially quantified+type variables of a constructor by filtering out those constructor-bound+variables which do not appear in the substitution that mergeArguments+returns. In this example, Refl's bound variables are k2 and a2. a2 appears+in the returned substitution, but k2 does not, which means that we would+mistakenly conclude that k2 is existential!++Although we don't have the full power of kind inference to guide us here, we+can at least do the next best thing. Generally, the datatype-bound type+variables and the constructor type variable binders contain all of the kind+information we need, so we proceed as follows:++1. Construct a map from each constructor-bound variable to its kind. (Do the+ same for each datatype-bound variable). These maps are the first and second+ arguments to closeOverKinds, respectively.+2. Call mergeArguments once on the GADT return type and datatype-bound types,+ and pass that in as the third argument to closeOverKinds.+3. For each name-name pair in the supplied substitution, check if the first and+ second names map to kinds in the first and second kind maps in+ closeOverKinds, respectively. If so, associate the first kind with the+ second kind.+4. For each kind association discovered in part (3), call mergeArguments+ on the lists of kinds. This will yield a kind substitution and kind+ equality context.+5. If the kind substitution is non-empty, then go back to step (3) and repeat+ the process on the new kind substitution and context.++ Otherwise, if the kind substitution is empty, then we have reached a fixed-+ point (i.e., we have closed over the kinds), so proceed.+6. Union up all of the substitutions and contexts, and return those.++This algorithm is not perfect, as it will only catch everything if all of+the kinds are explicitly mentioned somewhere (and not left quantified+implicitly). Thankfully, reifying data types via Template Haskell tends to+yield a healthy amount of kind signatures, so this works quite well in+practice.+-}+closeOverKinds :: Map Name Kind+ -> Map Name Kind+ -> (Map Name Name, Cxt)+ -> (Map Name Name, Cxt)+closeOverKinds domainFVKinds rangeFVKinds = go+ where+ go :: (Map Name Name, Cxt) -> (Map Name Name, Cxt)+ go (subst, context) =+ let substList = Map.toList subst+ (kindsInner, kindsOuter) =+ unzip $+ mapMaybe (\(d, r) -> do d' <- Map.lookup d domainFVKinds+ r' <- Map.lookup r rangeFVKinds+ return (d', r'))+ substList+ (kindSubst, kindContext) = mergeArgumentKinds kindsOuter kindsInner+ (restSubst, restContext)+ = if Map.null kindSubst -- Fixed-point calculation+ then (Map.empty, [])+ else go (kindSubst, kindContext)+ finalSubst = Map.unions [subst, kindSubst, restSubst]+ finalContext = nub $ concat [context, kindContext, restContext]+ -- Use `nub` here in an effort to minimize the number of+ -- redundant equality constraints in the returned context.+ in (finalSubst, finalContext)++-- Look into a list of types and map each free variable name to its kind.+kindsOfFVsOfTypes :: [Type] -> Map Name Kind+kindsOfFVsOfTypes = foldMap go+ where+ go :: Type -> Map Name Kind+ go (ForallT {}) = error "`forall` type used in data family pattern"+ go (AppT t1 t2) = go t1 `Map.union` go t2+ go (SigT t k) =+ let kSigs =+#if MIN_VERSION_template_haskell(2,8,0)+ go k+#else+ Map.empty+#endif+ in case t of+ VarT n -> Map.insert n k kSigs+ _ -> go t `Map.union` kSigs+ go _ = Map.empty++-- Look into a list of type variable binder and map each free variable name+-- to its kind (also map the names that KindedTVs bind to their respective+-- kinds). This function considers the kind of a PlainTV to be *.+kindsOfFVsOfTvbs :: [TyVarBndr] -> Map Name Kind+kindsOfFVsOfTvbs = foldMap go+ where+ go :: TyVarBndr -> Map Name Kind+ go (PlainTV n) = Map.singleton n starK+ go (KindedTV n k) =+ let kSigs =+#if MIN_VERSION_template_haskell(2,8,0)+ kindsOfFVsOfTypes [k]+#else+ Map.empty+#endif+ in Map.insert n k kSigs+ mergeArguments :: [Type] {- ^ outer parameters -} -> [Type] {- ^ inner parameters (specializations ) -} ->@@ -953,6 +1071,19 @@ aux _ sc = sc +-- | A specialization of 'mergeArguments' to 'Kind'.+-- Needed only for backwards compatibility with older versions of+-- @template-haskell@.+mergeArgumentKinds ::+ [Kind] ->+ [Kind] ->+ (Map Name Name, Cxt)+#if MIN_VERSION_template_haskell(2,8,0)+mergeArgumentKinds = mergeArguments+#else+mergeArgumentKinds _ _ = (Map.empty, [])+#endif+ -- | Expand all of the type synonyms in a type. resolveTypeSynonyms :: Type -> Q Type resolveTypeSynonyms t =@@ -962,10 +1093,9 @@ case f of ConT n ->- do info <- reifyRecover n $ fail- "resolveTypeSynonyms: Cannot reify type synonym information"- case info of- TyConI (TySynD _ synvars def)+ do mbInfo <- reifyMaybe n+ case mbInfo of+ Just (TyConI (TySynD _ synvars def)) -> resolveTypeSynonyms $ expandSynonymRHS synvars xs def _ -> notTypeSynCase _ -> notTypeSynCase@@ -987,10 +1117,9 @@ resolvePredSynonyms = resolveTypeSynonyms #else resolvePredSynonyms (ClassP n ts) = do- info <- reifyRecover n $ fail- "resolvePredSynonyms: Cannot reify type synonym information"- case info of- TyConI (TySynD _ synvars def)+ mbInfo <- reifyMaybe n+ case mbInfo of+ Just (TyConI (TySynD _ synvars def)) -> resolvePredSynonyms $ typeToPred $ expandSynonymRHS synvars ts def _ -> ClassP n <$> mapM resolveTypeSynonyms ts resolvePredSynonyms (EqualP t1 t2) = do@@ -1181,7 +1310,30 @@ -- | Class for types that support type variable substitution. class TypeSubstitution a where- -- | Apply a type variable substitution+ -- | Apply a type variable substitution.+ --+ -- Note that 'applySubstitution' is /not/ capture-avoiding. To illustrate+ -- this, observe that if you call this function with the following+ -- substitution:+ --+ -- * @b :-> a@+ --+ -- On the following 'Type':+ --+ -- * @forall a. b@+ --+ -- Then it will return:+ --+ -- * @forall a. a@+ --+ -- However, because the same @a@ type variable was used in the range of the+ -- substitution as was bound by the @forall@, the substituted @a@ is now+ -- captured by the @forall@, resulting in a completely different function.+ --+ -- For @th-abstraction@'s purposes, this is acceptable, as it usually only+ -- deals with globally unique type variable 'Name's. If you use+ -- 'applySubstitution' in a context where the 'Name's aren't globally unique,+ -- however, be aware of this potential problem. applySubstitution :: Map Name Type -> a -> a -- | Compute the free type variables freeVariables :: a -> [Name]@@ -1259,6 +1411,14 @@ applySubstitution _ k = k #endif +-- | Substitutes into the kinds of type variable binders.+-- Not capture-avoiding.+substTyVarBndrs :: Map Name Type -> [TyVarBndr] -> [TyVarBndr]+substTyVarBndrs subst = map go+ where+ go tvb@(PlainTV {}) = tvb+ go (KindedTV n k) = KindedTV n (applySubstitution subst k)+ ------------------------------------------------------------------------ combineSubstitutions :: Map Name Type -> Map Name Type -> Map Name Type@@ -1331,7 +1491,6 @@ ClassP #endif - -- | Match a 'Pred' representing an equality constraint. Returns -- arguments to the equality constraint if successful. asEqualPred :: Pred -> Maybe (Type,Type)@@ -1524,9 +1683,7 @@ _ -> Nothing #endif --- | Call 'reify' with an action to take if reification fails.-reifyRecover ::- Name ->- Q Info {- ^ handle failure -} ->- Q Info-reifyRecover n failure = failure `recover` reify n+-- | Call 'reify' and return @'Just' info@ if successful or 'Nothing' if+-- reification failed.+reifyMaybe :: Name -> Q (Maybe Info)+reifyMaybe n = return Nothing `recover` fmap Just (reify n)
test/Harness.hs view
@@ -23,6 +23,8 @@ import Control.Monad import qualified Data.Map as Map+import Data.Map (Map)+import Data.Maybe import Language.Haskell.TH import Language.Haskell.TH.Datatype import Language.Haskell.TH.Lib (starK)@@ -75,14 +77,21 @@ let sub1 = Map.fromList (zip (map tvName (constructorVars con2)) (map VarT (map tvName (constructorVars con1))))- sub2 = Map.fromList (zip (freeVariables con2)+ sub2 = Map.fromList (zip (freeVariables (map tvKind (constructorVars con2)))+ (map VarT (freeVariables+ (map tvKind (constructorVars con1)))))+ sub3 = Map.fromList (zip (freeVariables con2) (map VarT (freeVariables con1)))- sub = sub1 `Map.union` sub2+ sub = Map.unions [sub1, sub2, sub3] zipWithM_ (equateCxt "constructorContext") (constructorContext con1) (applySubstitution sub (constructorContext con2)) + check "constructorVars" id+ (constructorVars con1)+ (substIntoTyVarBndrs sub (constructorVars con2))+ check "constructorFields" id (constructorFields con1) (applySubstitution sub (constructorFields con2))@@ -97,6 +106,21 @@ NormalConstructor -> NormalConstructor i@InfixConstructor{} -> i RecordConstructor fields -> RecordConstructor $ map (mkName . nameBase) fields++ -- Substitutes both type variable names and kinds.+ substIntoTyVarBndrs :: Map Name Type -> [TyVarBndr] -> [TyVarBndr]+ substIntoTyVarBndrs subst = map go+ where+ go (PlainTV n) = PlainTV $ substName subst n+ go (KindedTV n k) = KindedTV (substName subst n)+ (applySubstitution subst k)++ substName :: Map Name Type -> Name -> Name+ substName subst n = fromMaybe n $ do+ nty <- Map.lookup n subst+ case nty of+ VarT n' -> Just n'+ _ -> Nothing equateStrictness :: FieldStrictness -> FieldStrictness -> Either String () equateStrictness fs1 fs2 =
test/Main.hs view
@@ -53,6 +53,9 @@ voidstosTest strictDemoTest recordVanillaTest+#if MIN_VERSION_template_haskell(2,6,0)+ t43Test+#endif #if MIN_VERSION_template_haskell(2,7,0) dataFamilyTest ghc78bugTest@@ -76,6 +79,10 @@ #if MIN_VERSION_template_haskell(2,8,0) kindSubstTest #endif+#if __GLASGOW_HASKELL__ >= 800+ t37Test+ polyKindedExTyvarTest+#endif regressionTest44 adt1Test :: IO ()@@ -215,7 +222,7 @@ , datatypeCons = [ ConstructorInfo { constructorName = 'Showable- , constructorVars = [PlainTV a]+ , constructorVars = [KindedTV a starK] , constructorContext = [classPred ''Show [VarT a]] , constructorFields = [VarT a] , constructorStrictness = [notStrictAnnot]@@ -319,6 +326,47 @@ $(do info <- reifyRecord 'gadtrec1a validateCI info gadtRecVanillaCI) +#if MIN_VERSION_template_haskell(2,6,0)+t43Test :: IO ()+t43Test =+ $(do [decPlain] <- [d| data T43Plain where MkT43Plain :: T43Plain |]+ infoPlain <- normalizeDec decPlain+ validateDI infoPlain+ DatatypeInfo+ { datatypeName = mkName "T43Plain"+ , datatypeContext = []+ , datatypeVars = []+ , datatypeVariant = Datatype+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = mkName "MkT43Plain"+ , constructorVars = []+ , constructorContext = []+ , constructorFields = []+ , constructorStrictness = []+ , constructorVariant = NormalConstructor } ]+ }++ [decFam] <- [d| data instance T43Fam where MkT43Fam :: T43Fam |]+ infoFam <- normalizeDec decFam+ validateDI infoFam+ DatatypeInfo+ { datatypeName = mkName "T43Fam"+ , datatypeContext = []+ , datatypeVars = []+ , datatypeVariant = DataInstance+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = mkName "MkT43Fam"+ , constructorVars = []+ , constructorContext = []+ , constructorFields = []+ , constructorStrictness = []+ , constructorVariant = NormalConstructor } ]+ }+ )+#endif+ #if MIN_VERSION_template_haskell(2,7,0) dataFamilyTest :: IO () dataFamilyTest =@@ -427,7 +475,7 @@ , constructorVariant = NormalConstructor } , ConstructorInfo { constructorName = '(:&&:)- , constructorVars = [PlainTV e]+ , constructorVars = [KindedTV e starK] , constructorContext = [equalPred cTy (AppT ListT eTy)] , constructorFields = [eTy,dTy] , constructorStrictness = [notStrictAnnot, notStrictAnnot]@@ -453,7 +501,7 @@ , constructorVariant = NormalConstructor } , ConstructorInfo { constructorName = 'MkGadtFam5- , constructorVars = [PlainTV q]+ , constructorVars = [KindedTV q starK] , constructorContext = [ equalPred cTy (ConT ''Bool) , equalPred dTy (ConT ''Bool) , equalPred qTy (ConT ''Char)@@ -587,9 +635,7 @@ , datatypeCons = [ ConstructorInfo { constructorName = 'Refl- , constructorVars = [KindedTV k starK]- -- This shouldn't happen, ideally. See #37.-+ , constructorVars = [] , constructorContext = [equalPred a b] , constructorFields = [] , constructorStrictness = []@@ -615,6 +661,97 @@ checkFreeVars ty [k1] checkFreeVars substTy [k2] [| return () |])+#endif++#if __GLASGOW_HASKELL__ >= 800+t37Test :: IO ()+t37Test =+ $(do infoA <- reifyDatatype ''T37a+ let [k,a] = map (VarT . mkName) ["k","a"]+ validateDI infoA+ DatatypeInfo+ { datatypeContext = []+ , datatypeName = ''T37a+ , datatypeVars = [SigT k starK, SigT a k]+ , datatypeVariant = Datatype+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = 'MkT37a+ , constructorVars = []+ , constructorContext = [equalPred k (ConT ''Bool)]+ , constructorFields = []+ , constructorStrictness = []+ , constructorVariant = NormalConstructor } ]+ }++ infoB <- reifyDatatype ''T37b+ validateDI infoB+ DatatypeInfo+ { datatypeContext = []+ , datatypeName = ''T37b+ , datatypeVars = [SigT a k]+ , datatypeVariant = Datatype+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = 'MkT37b+ , constructorVars = []+ , constructorContext = [equalPred k (ConT ''Bool)]+ , constructorFields = []+ , constructorStrictness = []+ , constructorVariant = NormalConstructor } ]+ }++ infoC <- reifyDatatype ''T37c+ validateDI infoC+ DatatypeInfo+ { datatypeContext = []+ , datatypeName = ''T37c+ , datatypeVars = [SigT a k]+ , datatypeVariant = Datatype+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = 'MkT37c+ , constructorVars = []+ , constructorContext = [equalPred a (ConT ''Bool)]+ , constructorFields = []+ , constructorStrictness = []+ , constructorVariant = NormalConstructor } ]+ }+ )++polyKindedExTyvarTest :: IO ()+polyKindedExTyvarTest =+ $(do info <- reifyDatatype ''T48+ let [a,x] = map mkName ["a","x"]+ validateDI info+ DatatypeInfo+ { datatypeContext = []+ , datatypeName = ''T48+ , datatypeVars = [SigT (VarT a) starK]+ , datatypeVariant = Datatype+ , datatypeCons =+ [ ConstructorInfo+ { constructorName = 'MkT48+ , constructorVars = [KindedTV x (VarT a)]+ , constructorContext = []+ , constructorFields = [ConT ''Prox `AppT` VarT x]+ , constructorStrictness = [notStrictAnnot]+ , constructorVariant = NormalConstructor } ]+ }+ -- Because validateCI uses a type variable substitution to normalize+ -- away any alpha-renaming differences between constructors, it+ -- unfortunately does not check if the uses of `a` in datatypeVars and+ -- constructorVars are the same. We perform this check explicitly here.+ case info of+ DatatypeInfo { datatypeVars = [SigT (VarT a1) starK]+ , datatypeCons =+ [ ConstructorInfo+ { constructorVars = [KindedTV _ (VarT a2)] } ] } ->+ unless (a1 == a2) $+ fail $ "Two occurrences of the same variable have different names: "+ ++ show [a1, a2]+ [| return () |]+ ) #endif regressionTest44 :: IO ()
test/Types.hs view
@@ -1,4 +1,4 @@-{-# Language CPP, FlexibleContexts, TypeFamilies, KindSignatures, TemplateHaskell, GADTs #-}+{-# Language CPP, FlexibleContexts, TypeFamilies, KindSignatures, TemplateHaskell, GADTs, ScopedTypeVariables #-} #if __GLASGOW_HASKELL__ >= 704 {-# LANGUAGE ConstraintKinds #-}@@ -8,6 +8,10 @@ {-# Language PolyKinds #-} #endif +#if __GLASGOW_HASKELL__ >= 800+{-# Language TypeInType #-}+#endif+ {-| Module : Types Description : Test cases for the th-abstraction package@@ -25,10 +29,14 @@ import GHC.Exts (Constraint) #endif -import Language.Haskell.TH+import Language.Haskell.TH hiding (Type) import Language.Haskell.TH.Datatype import Language.Haskell.TH.Lib (starK) +#if __GLASGOW_HASKELL__ >= 800+import Data.Kind+#endif+ type Gadt1Int = Gadt1 Int infixr 6 :**:@@ -60,10 +68,10 @@ data StrictDemo = StrictDemo Int !Int {-# UNPACK #-} !Int -#if MIN_VERSION_template_haskell(2,7,0)- -- Data families+data family T43Fam +#if MIN_VERSION_template_haskell(2,7,0) data family DF (a :: *) data instance DF (Maybe a) = DFMaybe Int [a] @@ -110,6 +118,22 @@ PredSyn1 Int Int => MkPredSynT1 Int | PredSyn2 Int Int => MkPredSynT2 Int | PredSyn3 Int => MkPredSynT3 Int+#endif++#if __GLASGOW_HASKELL__ >= 800+data T37a (k :: Type) :: k -> Type where+ MkT37a :: T37a Bool a++data T37b (a :: k) where+ MkT37b :: forall (a :: Bool). T37b a++data T37c (a :: k) where+ MkT37c :: T37c Bool++data Prox (a :: k) = Prox++data T48 :: Type -> Type where+ MkT48 :: forall a (x :: a). Prox x -> T48 a #endif -- We must define these here due to Template Haskell staging restrictions
th-abstraction.cabal view
@@ -1,5 +1,5 @@ name: th-abstraction-version: 0.2.7.0+version: 0.2.8.0 synopsis: Nicer interface for reified information about data types description: This package normalizes variations in the interface for inspecting datatype information via Template Haskell