diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 diff --git a/src/Language/Haskell/TH/Datatype.hs b/src/Language/Haskell/TH/Datatype.hs --- a/src/Language/Haskell/TH/Datatype.hs +++ b/src/Language/Haskell/TH/Datatype.hs @@ -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) diff --git a/test/Harness.hs b/test/Harness.hs --- a/test/Harness.hs +++ b/test/Harness.hs @@ -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 = diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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 () diff --git a/test/Types.hs b/test/Types.hs --- a/test/Types.hs +++ b/test/Types.hs @@ -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 diff --git a/th-abstraction.cabal b/th-abstraction.cabal --- a/th-abstraction.cabal +++ b/th-abstraction.cabal @@ -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