From c7b460412fe9896597270be94a243972833c0a66 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 6 Jul 2024 20:51:45 -0400 Subject: [PATCH] Improve local reification and desugaring with respect to standalone kind signatures Previously, `th-desugar` would not take standalone kind signatures into account when locally reifying a class method (#220). Similarly, it would not take them into account when locally reifying or desugaring a data constructor (#199). This patch accomplishes this, mainly by using the `matchUpSAKWithDecl` function (during local reification) and the `dMatchUpSAKWithDecl` function (during desugaring) to match up kind information from the standalone kind signature to the parent declaration's type variable binders. Fixes #199. Fixes #220. --- CHANGES.md | 34 +++++ Language/Haskell/TH/Desugar/Core.hs | 38 +++-- Language/Haskell/TH/Desugar/Reify.hs | 216 ++++++++++++++++++++++----- Test/Run.hs | 80 ++++++++++ 4 files changed, 314 insertions(+), 54 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 86ab535..b4b5d77 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,6 +52,40 @@ Version 1.18 [????.??.??] * Also add `matchUpSAKWithDecl`, `tvbForAllTyFlagsToSpecs`, and `tvbForAllTyFlagsToBndrVis` functions, which work over `TyVarBndr` instead of `DTyVarBndr`. +* Local reifying the type of a data constructor or class method now yields type + signatures with more precise type variable information, as `th-desugar` now + incorporates information from the standalone kind signature (if any) for the + parent data type or class, respectively. For instance, consider the following + data type declaration: + + ```hs + type P :: forall {k}. k -> Type + data P (a :: k) = MkP + ``` + + In previous versions of `th-desugar`, locally reifying `MkP` would yield the + following type: + + ```hs + MkP :: forall k (a :: k). P a + ``` + + This was subtly wrong, as `k` is marked as specified (i.e., eligible for + visible type application), not inferred. In `th-desugar-1.18`, however, the + locally reified type will mark `k` as inferred, as expected: + + ```hs + MkP :: forall {k} (a :: k). P a + ``` + + Similarly, desugaring `MkP` from Template Haskell to `th-desugar` results + in a data constructor with the expected type above. + * As a result of these changes, the type of `dsCon` has changed slightly: + + ```diff + -dsCon :: DsMonad q => [DTyVarBndrUnit] -> DType -> Con -> q [DCon] + +dsCon :: DsMonad q => [DTyVarBndrSpec] -> DType -> Con -> q [DCon] + ``` Version 1.17 [2024.05.12] ------------------------- diff --git a/Language/Haskell/TH/Desugar/Core.hs b/Language/Haskell/TH/Desugar/Core.hs index 0b50b81..2c2265c 100644 --- a/Language/Haskell/TH/Desugar/Core.hs +++ b/Language/Haskell/TH/Desugar/Core.hs @@ -827,12 +827,25 @@ dsDataDec :: DsMonad q -> Maybe Kind -> [Con] -> [DerivingClause] -> q [DDec] dsDataDec nd cxt n tvbs mk cons derivings = do tvbs' <- mapM dsTvbVis tvbs - let h98_tvbs = case mk of - -- If there's an explicit return kind, we're dealing with a - -- GADT, so this argument goes unused in dsCon. - Just {} -> unusedArgument - Nothing -> tvbs' - h98_return_type = nonFamilyDataReturnType n tvbs' + h98_tvbs <- + case mk of + -- If there's an explicit return kind, we're dealing with a + -- GADT, so this argument goes unused in dsCon. + Just {} -> pure unusedArgument + -- If there is no explicit return kind, we're dealing with a + -- Haskell98-style data type, so we must compute the type variable + -- binders to use in the types of the data constructors. + -- + -- Rather than just returning `tvbs'` here, we propagate kind information + -- from the data type's standalone kind signature (if one exists) to make + -- the kinds more precise. + Nothing -> do + mb_sak <- dsReifyType n + let tvbSpecs = changeDTVFlags SpecifiedSpec tvbs' + pure $ maybe tvbSpecs dtvbForAllTyFlagsToSpecs $ do + sak <- mb_sak + dMatchUpSAKWithDecl sak tvbs' + let h98_return_type = nonFamilyDataReturnType n tvbs' (:[]) <$> (DDataD nd <$> dsCxt cxt <*> pure n <*> pure tvbs' <*> mapM dsType mk <*> concatMapM (dsCon h98_tvbs h98_return_type) cons @@ -847,7 +860,7 @@ dsDataInstDec nd cxt n mtvbs tys mk cons derivings = do tys' <- mapM dsTypeArg tys let lhs' = applyDType (DConT n) tys' h98_tvbs = - changeDTVFlags defaultBndrFlag $ + changeDTVFlags SpecifiedSpec $ case (mk, mtvbs') of -- If there's an explicit return kind, we're dealing with a -- GADT, so this argument goes unused in dsCon. @@ -997,10 +1010,10 @@ dsTopLevelLetDec = fmap (map DLetDec . fst) . dsLetDec -- we require passing these as arguments. (If we desugar an actual GADT -- constructor, these arguments are ignored.) dsCon :: DsMonad q - => [DTyVarBndrVis] -- ^ The universally quantified type variables - -- (used if desugaring a non-GADT constructor). - -> DType -- ^ The original data declaration's type - -- (used if desugaring a non-GADT constructor). + => [DTyVarBndrSpec] -- ^ The universally quantified type variables + -- (used if desugaring a non-GADT constructor). + -> DType -- ^ The original data declaration's type + -- (used if desugaring a non-GADT constructor). -> Con -> q [DCon] dsCon univ_dtvbs data_type con = do dcons' <- dsCon' con @@ -1008,8 +1021,7 @@ dsCon univ_dtvbs data_type con = do case m_gadt_type of Nothing -> let ex_dtvbs = dtvbs - expl_dtvbs = changeDTVFlags SpecifiedSpec univ_dtvbs ++ - ex_dtvbs + expl_dtvbs = univ_dtvbs ++ ex_dtvbs impl_dtvbs = changeDTVFlags SpecifiedSpec $ toposortKindVarsOfTvbs expl_dtvbs in DCon (impl_dtvbs ++ expl_dtvbs) dcxt n fields data_type diff --git a/Language/Haskell/TH/Desugar/Reify.hs b/Language/Haskell/TH/Desugar/Reify.hs index e7d76ed..434c98a 100644 --- a/Language/Haskell/TH/Desugar/Reify.hs +++ b/Language/Haskell/TH/Desugar/Reify.hs @@ -285,14 +285,25 @@ reifyInDec n _ dec@(TypeDataD n' _ _ _) | n `nameMatches` n' = Just (n', TyConI #endif reifyInDec n decs (DataD _ ty_name tvbs _mk cons _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + cons = Just info reifyInDec n decs (NewtypeD _ ty_name tvbs _mk con _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) [con] + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + [con] = Just info -reifyInDec n _decs (ClassD _ ty_name tvbs _ sub_decs) +reifyInDec n decs (ClassD _ cls_name cls_tvbs _ sub_decs) | Just (n', ty) <- findType n sub_decs - = Just (n', ClassOpI n (quantifyClassMethodType ty_name tvbs True ty) ty_name) + = Just (n', ClassOpI n + (quantifyClassMethodType + (matchUpSAKWithTvbsSpec decs cls_name cls_tvbs) + (applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)) + True ty) + cls_name) reifyInDec n decs (ClassD _ _ _ _ sub_decs) | Just info <- firstMatch (reifyInDec n decs) sub_decs -- Important: don't pass (sub_decs ++ decs) to reifyInDec @@ -312,32 +323,66 @@ reifyInDec n decs (PatSynD pat_syn_name args _ _) = Just (n', VarI n full_sel_ty Nothing) #endif #if __GLASGOW_HASKELL__ >= 807 -reifyInDec n decs (DataInstD _ _ lhs _ cons _) +reifyInDec n decs (DataInstD _ mtvbs lhs _ cons _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys cons + , Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbs mtvbs tys) + -- Why do we reapply `ty_name` to `tys` here instead of just + -- reusing `lhs`? See Note [Apply data family type + -- constructors in prefix form in local reification]. + (applyType (ConT ty_name) tys) + cons = Just info -reifyInDec n decs (NewtypeInstD _ _ lhs _ con _) +reifyInDec n decs (NewtypeInstD _ mtvbs lhs _ con _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys [con] + , Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbs mtvbs tys) + -- Why do we reapply `ty_name` to `tys` here instead of just + -- reusing `lhs`? See Note [Apply data family type + -- constructors in prefix form in local reification]. + (applyType (ConT ty_name) tys) + [con] = Just info #else reifyInDec n decs (DataInstD _ ty_name tys _ cons _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) cons + | Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbsNoInstTvbs tys) + (applyType (ConT ty_name) (map TANormal tys)) + cons = Just info reifyInDec n decs (NewtypeInstD _ ty_name tys _ con _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) [con] + | Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbsNoInstTvbs tys) + (applyType (ConT ty_name) (map TANormal tys)) + [con] = Just info #endif #if __GLASGOW_HASKELL__ >= 906 reifyInDec n decs (TypeDataD ty_name tvbs _mk cons) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + cons = Just info #endif reifyInDec _ _ _ = Nothing -maybeReifyCon :: Name -> [Dec] -> Name -> [TypeArg] -> [Con] -> Maybe (Named Info) -maybeReifyCon n _decs ty_name ty_args cons +maybeReifyCon :: + Name + -> [Dec] + -> Name + -> [TyVarBndrSpec] + -- ^ The universally quantified type variables, derived from the parent + -- data declaration. This is only used if reifying a Haskell98-style data + -- constructor. + -> Type + -- ^ The data constructor's return type, derived from the parent data + -- declaration. This is only used if reifying a Haskell98-style data + -- constructor. + -> [Con] + -> Maybe (Named Info) +maybeReifyCon n _decs ty_name h98_tvbs h98_res_ty cons | Just (n', con) <- findCon n cons -- See Note [Use unSigType in maybeReifyCon] , let full_con_ty = unSigType $ con_to_type h98_tvbs h98_res_ty con @@ -357,7 +402,10 @@ maybeReifyCon n _decs ty_name ty_args cons extract_rec_sel_info rec_sel_info = case rec_sel_info of RecSelH98 sel_ty -> - ( changeTVFlags SpecifiedSpec h98_tvbs + let -- All of the type variables bound by the data type, with any + -- implicitly quantified kind variables made explicit. + all_h98_tvbs = quantifyAllTvbsSpec h98_tvbs in + ( all_h98_tvbs , sel_ty , h98_res_ty ) @@ -376,11 +424,7 @@ maybeReifyCon n _decs ty_name ty_args cons , con_res_ty ) - h98_tvbs = freeVariablesWellScoped $ - map probablyWrongUnTypeArg ty_args - h98_res_ty = applyType (ConT ty_name) ty_args - -maybeReifyCon _ _ _ _ _ = Nothing +maybeReifyCon _ _ _ _ _ _ = Nothing #if __GLASGOW_HASKELL__ >= 801 -- | Attempt to reify the type of a pattern synonym record selector @n@. @@ -539,10 +583,36 @@ Then the type of unD will be reified as: This is contrast to GHC's own reification, which will produce `D a` (without the explicit kind signature) as the type of the first argument. + +Note [Apply data family type constructors in prefix form in local reification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we wish to locally reify the type of `MkD` below: + + data family a :&: b + data instance a :&: b = MkD a b + +You might be tempted to think that the return type should be: + + MkD :: a -> b -> a :&: b + +However, keep in mind that local reification tries its best to mimic GHC's +behavior when reifying global declarations using Template Haskell. As it turns +out, if `MkD` were defined globally, then Template Haskell would reify it as: + + MkD :: a -> b -> (:&:) a b + +Note that `(:&:)` is applied prefix, not infix! This is somewhat surprising, +but nevertheless valid code. We mimic this surprising behavior when locally +reifying data family instances such as (:&:). This means that we cannot just +reuse the type `a :&: b` in the return type of `MkD`. Instead, we must +decompose `a :&: b` into its type arguments and apply (:&:) (in prefix form) to +the type arguments. + +The R40 test case checks for this property. -} -- Reverse-engineer the type of a data constructor. -con_to_type :: [TyVarBndrUnit] -- The type variables bound by a data type head. +con_to_type :: [TyVarBndrSpec] -- The type variables bound by a data type head. -- Only used for Haskell98-style constructors. -> Type -- The constructor result type. -- Only used for Haskell98-style constructors. @@ -550,9 +620,7 @@ con_to_type :: [TyVarBndrUnit] -- The type variables bound by a data type head. con_to_type h98_tvbs h98_result_ty con = case go con of (is_gadt, ty) | is_gadt -> ty - | otherwise -> maybeForallT - (changeTVFlags SpecifiedSpec h98_tvbs) - [] ty + | otherwise -> maybeForallT all_h98_tvbs [] ty where -- Note that we deliberately ignore linear types and use (->) everywhere. -- See [Gracefully handling linear types] in L.H.TH.Desugar.Core. @@ -564,6 +632,11 @@ con_to_type h98_tvbs h98_result_ty con = go (GadtC _ stys rty) = (True, mkArrows (map snd stys) rty) go (RecGadtC _ vstys rty) = (True, mkArrows (map thdOf3 vstys) rty) + -- All of the type variables bound by the data type, with any implicitly + -- quantified kind variables made explicit. + all_h98_tvbs :: [TyVarBndrSpec] + all_h98_tvbs = quantifyAllTvbsSpec h98_tvbs + mkVarI :: Name -> [Dec] -> Info mkVarI n decs = mkVarITy n (maybe (no_type n) snd $ findType n decs) @@ -712,7 +785,11 @@ quantifyClassDecMethods (ClassD cxt cls_name cls_tvbs fds sub_decs) sub_decs' = mapMaybe go sub_decs go (SigD n ty) = Just $ SigD n - $ quantifyClassMethodType cls_name cls_tvbs prepend_cls ty + $ quantifyClassMethodType + (changeTVFlags SpecifiedSpec cls_tvbs) + (applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)) + prepend_cls + ty go d@(TySynInstD {}) = Just d go d@(OpenTypeFamilyD {}) = Just d go d@(DataFamilyD {}) = Just d @@ -733,8 +810,8 @@ quantifyClassDecMethods dec = dec -- [d| class C a where -- method :: a -> b -> a |] -- --- If one invokes `quantifyClassMethodType C [a] prepend (a -> b -> a)`, then --- the output will be: +-- If one invokes `quantifyClassMethodType [a] (C a) prepend (a -> b -> a)`, +-- then the output will be: -- -- 1. `forall a. C a => forall b. a -> b -> a` (if `prepend` is True) -- 2. `forall b. a -> b -> a` (if `prepend` is False) @@ -746,22 +823,19 @@ quantifyClassDecMethods dec = dec -- a single class method, like `method`, then one needs the class context to -- appear in the reified type, so `True` is appropriate. quantifyClassMethodType - :: Name -- ^ The class name. - -> [TyVarBndrVis] -- ^ The class's type variable binders. - -> Bool -- ^ If 'True', prepend a class predicate. - -> Type -- ^ The method type. + :: [TyVarBndrSpec] -- ^ The class's type variable binders. + -> Pred -- ^ The class context. + -> Bool -- ^ If 'True', prepend a class predicate. + -> Type -- ^ The method type. -> Type -quantifyClassMethodType cls_name cls_tvbs prepend meth_ty = +quantifyClassMethodType cls_tvbs cls_pred prepend meth_ty = add_cls_cxt quantified_meth_ty where add_cls_cxt :: Type -> Type add_cls_cxt - | prepend = ForallT (changeTVFlags SpecifiedSpec all_cls_tvbs) cls_cxt + | prepend = ForallT all_cls_tvbs [cls_pred] | otherwise = id - cls_cxt :: Cxt - cls_cxt = [applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)] - quantified_meth_ty :: Type quantified_meth_ty | null meth_tvbs @@ -772,13 +846,15 @@ quantifyClassMethodType cls_name cls_tvbs prepend meth_ty = = ForallT meth_tvbs [] meth_ty meth_tvbs :: [TyVarBndrSpec] - meth_tvbs = changeTVFlags SpecifiedSpec $ - List.deleteFirstsBy ((==) `on` tvName) - (freeVariablesWellScoped [meth_ty]) all_cls_tvbs + meth_tvbs = List.deleteFirstsBy ((==) `on` tvName) + (changeTVFlags SpecifiedSpec + (freeVariablesWellScoped [meth_ty])) + all_cls_tvbs - -- Explicitly quantify any kind variables bound by the class, if any. - all_cls_tvbs :: [TyVarBndrUnit] - all_cls_tvbs = freeVariablesWellScoped $ map tvbToTypeWithSig cls_tvbs + -- All of the type variables bound by the class, with any implicitly + -- quantified kind variables made explicit. + all_cls_tvbs :: [TyVarBndrSpec] + all_cls_tvbs = quantifyAllTvbsSpec cls_tvbs stripInstanceDec :: Dec -> Dec stripInstanceDec (InstanceD over cxt ty _) = InstanceD over cxt ty [] @@ -876,6 +952,64 @@ findRecSelector n = firstMatch (match_con Nothing) where ret_fvs = Set.fromList $ freeVariables [ret_ty] +-- | Match up the type variable binders from a data type or class declaration +-- with its standalone kind signature (if any) to produce a list of +-- 'TyVarBndrSpec's, which can then be used in the types of data constructors or +-- class methods. This makes the kinds more precise. +matchUpSAKWithTvbsSpec :: + [Dec] + -- ^ The local declarations currently in scope. + -> Name + -- ^ The name of the data type or class declaration. + -> [TyVarBndrVis] + -- ^ The data type or class declaration's type variable binders. + -> [TyVarBndrSpec] +matchUpSAKWithTvbsSpec decs ty_name tvbs = + fromMaybe (changeTVFlags SpecifiedSpec tvbs) $ do + sak <- findKind False ty_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl sak tvbs + +-- | Compute the type variable binders to use in the type of a Haskell98-style +-- data constructor for a data family instance. If the data family instance +-- comes equipped with explicit type variable binders, this is easy. If not, +-- we must compute the type variable binders from the list of type arguments to +-- the data family instance. +dataFamInstH98ConTvbs :: Maybe [TyVarBndrUnit] -> [TypeArg] -> [TyVarBndrSpec] +dataFamInstH98ConTvbs mtvbs tys = + case mtvbs of + Just tvbs -> + changeTVFlags SpecifiedSpec tvbs + Nothing -> + dataFamInstH98ConTvbsNoInstTvbs $ + map probablyWrongUnTypeArg tys + +-- | Compute the type variable binders to use in the type of a Haskell98-style +-- data constructor for a data family instance where the instance lacks explicit +-- type variable binders. To compute these binders, we must reverse engineer +-- them from the list of type arguments to the data family instance. +dataFamInstH98ConTvbsNoInstTvbs :: [Type] -> [TyVarBndrSpec] +dataFamInstH98ConTvbsNoInstTvbs tys = + changeTVFlags SpecifiedSpec $ + freeVariablesWellScoped tys + +-- | Explicitly quantify all type variable binders in the type of a +-- Haskell98-style data constructor or class method. This is sometimes required +-- in order to ensure that kind variables are all explicitly quantified, e.g., +-- +-- @ +-- -- NB: No standalone kind signature for `T` +-- data T (a :: k) = MkT +-- @ +-- +-- We want the type of @MkT@ to be @forall k (a :: k). T a@, but we are only +-- given @(a :: k)@. We must call 'quantifyAllTvbsSpec' on @(a :: k)@ to obtain +-- @[k, a :: k]@. If we don't, we might accidentally end up with +-- @forall (a :: k). T a@ as the type of @MkT@, which is ill-scoped. +quantifyAllTvbsSpec :: [TyVarBndrSpec] -> [TyVarBndrSpec] +quantifyAllTvbsSpec h98_tvbs = + let h98_kvbs = freeKindVariablesWellScoped h98_tvbs in + changeTVFlags SpecifiedSpec h98_kvbs ++ h98_tvbs + --------------------------------- -- Reifying fixities --------------------------------- diff --git a/Test/Run.hs b/Test/Run.hs index 194fe42..c35b666 100644 --- a/Test/Run.hs +++ b/Test/Run.hs @@ -72,6 +72,7 @@ import qualified Data.Map as M import Data.Proxy #if __GLASGOW_HASKELL__ >= 900 +import Data.Kind (Constraint) import Prelude as P #endif @@ -696,6 +697,46 @@ test_t188 = toposortKindVarsOfTvbs [DKindedTV a1 () (DVarT a2), DKindedTV a2 () (DVarT a1)] == [DPlainTV a2 ()] +#if __GLASGOW_HASKELL__ >= 900 +-- A regression test for #199, which ensures that a locally reified data +-- constructor is given a type signature that takes into account the fact that +-- its parent data type's standalone kind signature marks `k` as inferred. +test_t199 :: [Bool] +test_t199 = + $(do decs <- [d| type P :: forall {k}. k -> Type + data P (a :: k) = MkP |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + p = mkName "P" + mkP = mkName "MkP" + pTy = DConT p `DAppT` DVarT a + mbPInfo <- dsReify p + let b1 = + case mbPInfo of + Just (DTyConI (DDataD _ _ _ _ _ [conActual] _) _) -> + let conExpected = + DCon [kTvb, aTvb] [] mkP (DNormalC False []) pTy in + conExpected `eqTH` conActual + _ -> + False + + mbMkPInfo <- dsReify mkP + let b2 = + case mbMkPInfo of + Just (DVarI _ conTyActual _) -> + let conTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) pTy in + conTyExpected `eqTH` conTyActual + _ -> + False + + [| [b1, b2] |]) +#endif + -- Unit tests for unboxedTupleNameDegree_maybe and unboxedSumNameDegree_maybe. -- These also act as a regression test for #213. test_t213 :: [Bool] @@ -740,6 +781,36 @@ test_t213 = ] #endif +#if __GLASGOW_HASKELL__ >= 900 +-- A regression test for #220, which ensures that a locally reified class method +-- is given a type signature that takes into account the fact that its parent +-- class's standalone kind signature marks `k` as inferred. +test_t220 :: Bool +test_t220 = + $(do decs <- [d| type C :: forall {k}. k -> Constraint + class C (a :: k) where + m :: Proxy a |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + c = mkName "C" + m = mkName "m" + cTy = DConT c `DAppT` DVarT a + mbMInfo <- dsReify m + case mbMInfo of + Just (DVarI _ mTyActual _) -> + let mTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) $ + DConstrainedT [cTy] $ + DConT ''Proxy `DAppT` DVarT a in + mTyExpected `eqTHSplice` mTyActual + _ -> + [| False |]) +#endif + -- Unit tests for functions that compute free variables (e.g., fvDType) test_fvs :: [Bool] test_fvs = @@ -979,9 +1050,18 @@ main = hspec $ do it "computes free kind variables correctly in a telescope that uses shadowing" $ test_t188 +#if __GLASGOW_HASKELL__ >= 900 + zipWithM (\b n -> it ("correctly reifies the type of a data constructor with an inferred type variable binder " ++ show n) b) + test_t199 [1..] +#endif + zipWithM (\b n -> it ("recognizes unboxed {tuple,sum} names with unboxed{Tuple,Sum}Degree_maybe correctly " ++ show n) b) test_t213 [1..] +#if __GLASGOW_HASKELL__ >= 900 + it "correctly reifies the type of a class method with an inferred type variable binder" $ test_t220 +#endif + -- Remove map pprints here after switch to th-orphans zipWithM (\t t' -> it ("can do Type->DType->Type of " ++ t) $ t == t') $(sequence round_trip_types >>= Syn.lift . map pprint)