diff options
| -rw-r--r-- | compiler/GHC/Core/DataCon.hs | 1 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Pat.hs | 327 | ||||
| -rw-r--r-- | testsuite/tests/gadt/T19847.hs | 15 | ||||
| -rw-r--r-- | testsuite/tests/gadt/T19847a.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/gadt/T19847a.stderr | 12 | ||||
| -rw-r--r-- | testsuite/tests/gadt/all.T | 2 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T19577.hs | 24 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T21501.hs | 24 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T22383.hs | 83 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 3 |
10 files changed, 400 insertions, 105 deletions
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs index 1ed274e078..1473221226 100644 --- a/compiler/GHC/Core/DataCon.hs +++ b/compiler/GHC/Core/DataCon.hs @@ -441,6 +441,7 @@ data DataCon -- INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders is -- exactly the set of tyvars (*not* covars) of dcExTyCoVars unioned -- with the set of dcUnivTyVars whose tyvars do not appear in dcEqSpec + -- So dcUserTyVarBinders is a subset of (dcUnivTyVars ++ dcExTyCoVars) -- See Note [DataCon user type variable binders] dcUserTyVarBinders :: [InvisTVBinder], diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 35c2463cb6..28b9891b91 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -72,9 +72,12 @@ import Control.Arrow ( second ) import Control.Monad import GHC.Data.FastString import qualified Data.List.NonEmpty as NE + import GHC.Data.List.SetOps ( getNth ) import Language.Haskell.Syntax.Basic (FieldLabelString(..)) +import Data.List( partition ) + {- ************************************************************************ * * @@ -315,6 +318,11 @@ type Checker inp out = forall r. , r -- Result of thing inside ) +tcMultiple_ :: Checker inp () -> PatEnv -> [inp] -> TcM r -> TcM r +tcMultiple_ tc_pat penv args thing_inside + = do { (_, res) <- tcMultiple tc_pat penv args thing_inside + ; return res } + tcMultiple :: Checker inp out -> Checker [inp] [out] tcMultiple tc_pat penv args thing_inside = do { err_ctxt <- getErrCtxt @@ -861,10 +869,10 @@ tcConPat :: PatEnv -> LocatedN Name tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside = do { con_like <- tcLookupConLike con_name ; case con_like of - RealDataCon data_con -> tcDataConPat penv con_lname data_con - pat_ty arg_pats thing_inside - PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn - pat_ty arg_pats thing_inside + RealDataCon data_con -> tcDataConPat con_lname data_con pat_ty + penv arg_pats thing_inside + PatSynCon pat_syn -> tcPatSynPat con_lname pat_syn pat_ty + penv arg_pats thing_inside } -- Warn when pattern matching on a GADT or a pattern synonym @@ -880,12 +888,11 @@ warnMonoLocalBinds -- In #20485 this was made into a warning. } -tcDataConPat :: PatEnv -> LocatedN Name -> DataCon +tcDataConPat :: LocatedN Name -> DataCon -> Scaled ExpSigmaTypeFRR -- Type of the pattern - -> HsConPatDetails GhcRn -> TcM a - -> TcM (Pat GhcTc, a) -tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled - arg_pats thing_inside + -> Checker (HsConPatDetails GhcRn) (Pat GhcTc) +tcDataConPat (L con_span con_name) data_con pat_ty_scaled + penv arg_pats thing_inside = do { let tycon = dataConTyCon data_con -- For data families this is the representation tycon (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) @@ -921,21 +928,15 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled -- Why "super"? See Note [Binding when looking up instances] -- in GHC.Core.InstEnv. - ; let arg_tys' = substScaledTys tenv arg_tys - pat_mult = scaledMult pat_ty_scaled + ; let arg_tys' = substScaledTys tenv arg_tys + pat_mult = scaledMult pat_ty_scaled arg_tys_scaled = map (scaleScaled pat_mult) arg_tys' + con_like = RealDataCon data_con -- This check is necessary to uphold the invariant that 'tcConArgs' -- is given argument types with a fixed runtime representation. -- See test case T20363. - ; zipWithM_ - ( \ i arg_sty -> - hasFixedRuntimeRep_syntactic - (FRRDataConPatArg data_con i) - (scaledThing arg_sty) - ) - [1..] - arg_tys' + ; checkFixedRuntimeRep data_con arg_tys' ; traceTc "tcConPat" (vcat [ text "con_name:" <+> ppr con_name , text "univ_tvs:" <+> pprTyVars univ_tvs @@ -947,11 +948,15 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled , text "pat_ty:" <+> ppr pat_ty , text "arg_tys':" <+> ppr arg_tys' , text "arg_pats" <+> ppr arg_pats ]) + + ; (univ_ty_args, ex_ty_args) <- splitConTyArgs con_like arg_pats + ; if null ex_tvs && null eq_spec && null theta then do { -- The common case; no class bindings etc -- (see Note [Arrows and patterns]) - (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled - tenv penv arg_pats thing_inside + (arg_pats', res) <- tcConTyArgs tenv penv univ_ty_args $ + tcConValArgs con_like arg_tys_scaled + penv arg_pats thing_inside ; let res_pat = ConPat { pat_con = header , pat_args = arg_pats' , pat_con_ext = ConPatTc @@ -974,8 +979,11 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled ; given <- newEvVars theta' ; (ev_binds, (arg_pats', res)) - <- checkConstraints (getSkolemInfo skol_info) ex_tvs' given $ - tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside + <- -- See Note [Type applications in patterns] (W4) + tcConTyArgs tenv penv univ_ty_args $ + checkConstraints (getSkolemInfo skol_info) ex_tvs' given $ + tcConTyArgs tenv penv ex_ty_args $ + tcConValArgs con_like arg_tys_scaled penv arg_pats thing_inside ; let res_pat = ConPat { pat_con = header @@ -991,11 +999,10 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled ; return (mkHsWrapPat wrap res_pat pat_ty, res) } } -tcPatSynPat :: PatEnv -> LocatedN Name -> PatSyn +tcPatSynPat :: LocatedN Name -> PatSyn -> Scaled ExpSigmaType -- ^ Type of the pattern - -> HsConPatDetails GhcRn -> TcM a - -> TcM (Pat GhcTc, a) -tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside + -> Checker (HsConPatDetails GhcRn) (Pat GhcTc) +tcPatSynPat (L con_span con_name) pat_syn pat_ty penv arg_pats thing_inside = do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn ; (subst, univ_tvs') <- newMetaTyVars univ_tvs @@ -1018,23 +1025,27 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside arg_tys_scaled = map (scaleScaled pat_mult) arg_tys' prov_theta' = substTheta tenv prov_theta req_theta' = substTheta tenv req_theta + con_like = PatSynCon pat_syn ; when (any isEqPred prov_theta) warnMonoLocalBinds ; mult_wrap <- checkManyPattern pat_ty -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify. - ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty' - ; traceTc "tcPatSynPat" (ppr pat_syn $$ - ppr pat_ty $$ - ppr ty' $$ - ppr ex_tvs' $$ - ppr prov_theta' $$ - ppr req_theta' $$ - ppr arg_tys') + ; (univ_ty_args, ex_ty_args) <- splitConTyArgs con_like arg_pats - ; prov_dicts' <- newEvVars prov_theta' + ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty' + ; traceTc "tcPatSynPat" $ + vcat [ text "Pat syn:" <+> ppr pat_syn + , text "Expected type:" <+> ppr pat_ty + , text "Pat res ty:" <+> ppr ty' + , text "ex_tvs':" <+> pprTyVars ex_tvs' + , text "prov_theta':" <+> ppr prov_theta' + , text "req_theta':" <+> ppr req_theta' + , text "arg_tys':" <+> ppr arg_tys' + , text "univ_ty_args:" <+> ppr univ_ty_args + , text "ex_ty_args:" <+> ppr ex_ty_args ] ; req_wrap <- instCall (OccurrenceOf con_name) (mkTyVarTys univ_tvs') req_theta' -- Origin (OccurrenceOf con_name): @@ -1055,11 +1066,16 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside , text "bad_arg_tys:" <+> ppr bad_arg_tys ] ; traceTc "checkConstraints {" Outputable.empty + ; prov_dicts' <- newEvVars prov_theta' ; (ev_binds, (arg_pats', res)) - <- checkConstraints (getSkolemInfo skol_info) ex_tvs' prov_dicts' $ - tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside - + <- -- See Note [Type applications in patterns] (W4) + tcConTyArgs tenv penv univ_ty_args $ + checkConstraints (getSkolemInfo skol_info) ex_tvs' prov_dicts' $ + tcConTyArgs tenv penv ex_ty_args $ + tcConValArgs con_like arg_tys_scaled penv arg_pats $ + thing_inside ; traceTc "checkConstraints }" (ppr ev_binds) + ; let res_pat = ConPat { pat_con = L con_span $ PatSynCon pat_syn , pat_args = arg_pats' , pat_con_ext = ConPatTc @@ -1073,6 +1089,14 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat (wrap <.> mult_wrap) res_pat pat_ty, res) } +checkFixedRuntimeRep :: DataCon -> [Scaled TcSigmaTypeFRR] -> TcM () +checkFixedRuntimeRep data_con arg_tys + = zipWithM_ check_one [1..] arg_tys + where + check_one i arg_ty = hasFixedRuntimeRep_syntactic + (FRRDataConPatArg data_con i) + (scaledThing arg_ty) + {- Note [Call-stack tracing of pattern synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1187,84 +1211,128 @@ Suppose (coi, tys) = matchExpectedConType data_tc pat_ty error messages; it's a purely internal thing -} -{- -Note [Typechecking type applications in patterns] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -How should we typecheck type applications in patterns, such as +{- Note [Type applications in patterns] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Type applications in patterns are enabled by -XTypeAbstractions. +For example: f :: Either (Maybe a) [b] -> blah f (Left @x @[y] (v::Maybe x)) = blah -It's quite straightforward, and very similar to the treatment of -pattern signatures. +How should we typecheck them? The basic plan is pretty simple, and is +all done in tcConTyArgs. For each type argument: -* Step 1: bind the newly-in-scope type variables x and y to fresh - unification variables, say x0 and y0. +* Step 1: + * bind the newly-in-scope type variables (here `x` or `y`) to + unification variables, say `x0` or `y0` -* Step 2: typecheck those type arguments, @x and @[y], to get the - types x0 and [y0]. + * typecheck the type argument, `@x` or `@[y]` to get the + types `x0` or `[y0]`. -* Step 3: Unify those types with the type arguments we expect, - in this case (Maybe a) and [b]. These unifications will - (perhaps after the constraint solver has done its work) + This step is done by `tcHsPatSigType`, similar to the way we + deal with pattern signatures. + +* Step 2: Unify those types with the type arguments we expect from + the context, in this case (Maybe a) and [b]. These unifications + will (perhaps after the constraint solver has done its work) unify x0 := Maybe a y0 := b Thus we learn that x stands for (Maybe a) and y for b. -Wrinkles: - -* Surprisingly, we can discard the coercions arising from - these unifications. The *only* thing the unification does is - to side-effect those unification variables, so that we know - what type x and y stand for; and cause an error if the equality - is not soluble. It's a bit like a constraint arising - from a functional dependency, where we don't use the evidence. - -* Exactly the same works for existential arguments - data T where - MkT :: a -> a -> T - f :: T -> blah - f (MkT @x v w) = ... - Here we create a fresh unification variable x0 for x, and - unify it with the fresh existential variable bound by the pattern. - -* Note that both here and in pattern signatures the unification may - not even end up unifying the variable. For example - type S a b = a - f :: Maybe a -> Bool - f (Just @(S a b) x) = True :: b - In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no - effect on the unification variable b0, to which 'b' is bound. - Later, in the RHS, we find that b0 must be Bool, and unify it there. - All is fine. +* Step 3: Extend the lexical context to bind `x` to `x0` and + `y` to `y0`, and typecheck the body of the pattern match. + +However there are several quite tricky wrinkles. + +(W1) Surprisingly, we can discard the coercions arising from + these unifications. The *only* thing the unification does is + to side-effect those unification variables, so that we know + what type x and y stand for; and cause an error if the equality + is not soluble. It's a bit like a constraint arising + from a functional dependency, where we don't use the evidence. + +(W2) Note that both here and in pattern signatures the unification may + not even end up unifying the variable. For example + type S a b = a + f :: Maybe a -> Bool + f (Just @(S a b) x) = True :: b + In Step 2 we will unify (S a0 b0 ~ a), which succeeds, but has no + effect on the unification variable b0, to which 'b' is bound. + Later, in the RHS, we find that b0 must be Bool, and unify it there. + All is fine. + +(W3) The order of the arguments to the /data constructor/ may differ from + the order of the arguments to the /type constructor/. Example + data T a b where { MkT :: forall c d. (c,d) -> T d c } + f :: T Int Bool -> blah + f (MkT @x @y p) = ... + The /first/ type argument to `MkT`, namely `@x` corresponds to the + /second/ argument to `T` in the type `T Int Bool`. So `x` is bound + to `Bool` -- not to `Int`!. That is why splitConTyArgs uses + conLikeUserTyVarBinders to match up with the user-supplied type arguments + in the pattern, not dataConUnivTyVars/dataConExTyVars. + +(W4) A similar story works for existentials, but it is subtly different + (#19847). Consider + data T a where { MkT :: forall a b. a -> b -> T a } + f :: T Int -> blah + f (MkT @x @y v w) = blah + Here we create a fresh unification variables x0,y0 for x,y and + unify x0~Int, y0~b, where b is the fresh existential variable bound by + the pattern. But + * (x0~Int) must be /outside/ the implication constraint + * (y0~b) must be /inside/ it + (and hence x0 and y0 themselves must have different levels). + Thus: + x0[1]~Int, (forall[2] b. (y0[2]~b, ...constraints-from-blah...)) + + We need (x0~Int) /outside/ so that it can influence the type of the + pattern in an inferred setting, e.g. + g :: T _ -> blah + g (MkT @Int @y v w) = blah + Here we want to infer `g` to have type `T Int -> blah`. If the + (x0~Int) was inside the implication, and the the constructor bound + equality constraints, `x0` would be untouchable. This was the root + cause of #19847. + + We need (y0~b) to be /inside/ the implication, so that `b` is in + scope. In fact, we may actually /need/ equalities bound by the + implication to prove the equality constraint we generate. + Example data T a where + MkT :: forall p q. T (p,q) + f :: T (Int,Bool) -> blah + f (MkT @Int @Bool) = ... + We get the implication + forall[2] p q. (p,q)~(Int,Bool) => (p ~ Int, q ~ Bool, ...) + where the Given comes from the GADT match, while (p~Int, q~Bool) + comes from matching the type arguments. + + Wow. That's all quite subtle! See the long discussion on #19847. We + must treat universal and existential arguments separately, even though + they are all mixed up (W3). The function splitConTyArgs separates the + universals from existentials; and we build the implication between + typechecking the two sets: + tcConTyArgs ... univ_ty_args $ + checkConstraints ... $ + tcConTyArgs ... ex_ty_args $ + ..typecheck body.. + You can see this code shape in tcDataConPat and tcPatSynPat. + + Where pattern synonyms are involved, this two-level split may not be + enough. See #22328 for the story. -} -tcConArgs :: ConLike - -> [Scaled TcSigmaTypeFRR] - -> Subst -- Instantiating substitution for constructor type - -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc) -tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of +tcConValArgs :: ConLike + -> [Scaled TcSigmaTypeFRR] + -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc) +tcConValArgs con_like arg_tys penv con_args thing_inside = case con_args of PrefixCon type_args arg_pats -> do + -- NB: type_args already dealt with + -- See Note [Type applications in patterns] { checkTc (con_arity == no_of_args) -- Check correct arity (arityErr (text "constructor") con_like con_arity no_of_args) - -- forgetting to filter out inferred binders led to #20443 - ; let con_spec_binders = filter ((== SpecifiedSpec) . binderFlag) $ - conLikeUserTyVarBinders con_like - ; checkTc (type_args `leLength` con_spec_binders) - (TcRnTooManyTyArgsInConPattern con_like (length con_spec_binders) (length type_args)) - ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys - ; (type_args', (arg_pats', res)) - <- tcMultiple tcConTyArg penv type_args $ - tcMultiple tcConArg penv pats_w_tys thing_inside - - -- This unification is straight from Figure 7 of - -- "Type Variables in Patterns", Haskell'18 - ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $ - binderVars con_spec_binders) - -- OK to drop coercions here. These unifications are all about - -- guiding inference based on a user-written type annotation - -- See Note [Typechecking type applications in patterns] + ; (arg_pats', res) <- tcMultiple tcConArg penv pats_w_tys thing_inside ; return (PrefixCon type_args arg_pats', res) } where @@ -1321,23 +1389,72 @@ tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of -- dataConFieldLabels will be empty (and each field in the pattern -- will generate an error below). -tcConTyArg :: Checker (HsConPatTyArg GhcRn) TcType -tcConTyArg penv (HsConPatTyArg _ rn_ty) thing_inside + +splitConTyArgs :: ConLike -> HsConPatDetails GhcRn + -> TcM ( [(HsConPatTyArg GhcRn, TyVar)] -- Universals + , [(HsConPatTyArg GhcRn, TyVar)] ) -- Existentials +-- See Note [Type applications in patterns] (W4) +-- This function is monadic only because of the error check +-- for too many type arguments +splitConTyArgs con_like (PrefixCon type_args _) + = do { checkTc (type_args `leLength` con_spec_bndrs) + (TcRnTooManyTyArgsInConPattern con_like + (length con_spec_bndrs) (length type_args)) + ; if null ex_tvs -- Short cut common case + then return (bndr_ty_arg_prs, []) + else return (partition is_universal bndr_ty_arg_prs) } + where + ex_tvs = conLikeExTyCoVars con_like + con_spec_bndrs = [ tv | Bndr tv SpecifiedSpec <- conLikeUserTyVarBinders con_like ] + -- conLikeUserTyVarBinders: see (W3) in + -- Note [Type applications in patterns] + -- SpecifiedSpec: forgetting to filter out inferred binders led to #20443 + + bndr_ty_arg_prs = type_args `zip` con_spec_bndrs + -- The zip truncates to length(type_args) + + is_universal (_, tv) = not (tv `elem` ex_tvs) + -- See Note [DataCon user type variable binders] in GHC.Core.DataCon + -- especially INVARIANT(dataConTyVars). + +splitConTyArgs _ (RecCon {}) = return ([], []) -- No type args in RecCon +splitConTyArgs _ (InfixCon {}) = return ([], []) -- No type args in InfixCon + +tcConTyArgs :: Subst -> PatEnv -> [(HsConPatTyArg GhcRn, TyVar)] + -> TcM a -> TcM a +tcConTyArgs tenv penv prs thing_inside + = tcMultiple_ (tcConTyArg tenv) penv prs thing_inside + +tcConTyArg :: Subst -> Checker (HsConPatTyArg GhcRn, TyVar) () +tcConTyArg tenv penv (HsConPatTyArg _ rn_ty, con_tv) thing_inside = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind -- AnyKind is a bit suspect: it really should be the kind gotten -- from instantiating the constructor type. But this would be -- hard to get right, because earlier type patterns might influence -- the kinds of later patterns. In any case, it all gets checked - -- by the calls to unifyType in tcConArgs, which will also unify - -- kinds. + -- by the calls to unifyType below which unifies kinds + ; case NE.nonEmpty sig_ibs of Just sig_ibs_ne | inPatBind penv -> addErr (TcRnCannotBindTyVarsInPatBind sig_ibs_ne) _ -> pure () + + -- This unification is straight from Figure 7 of + -- "Type Variables in Patterns", Haskell'18 + -- OK to drop coercions here. These unifications are all about + -- guiding inference based on a user-written type annotation + -- See Note [Type applications in patterns] (W1) + ; _ <- unifyType Nothing arg_ty (substTyVar tenv con_tv) + ; result <- tcExtendNameTyVarEnv sig_wcs $ tcExtendNameTyVarEnv sig_ibs $ thing_inside - ; return (arg_ty, result) } + -- NB: Because we call tConTyArgs twice, once for universals and + -- once for existentials; so this brings things into scope + -- "out of left-right order". But it doesn't matter; the renamer + -- has dealt with all that. + + ; return ((), result) } tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc) tcConArg penv (arg_pat, Scaled arg_mult arg_ty) diff --git a/testsuite/tests/gadt/T19847.hs b/testsuite/tests/gadt/T19847.hs new file mode 100644 index 0000000000..6187038d02 --- /dev/null +++ b/testsuite/tests/gadt/T19847.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns, ScopedTypeVariables #-} + +module T19847 where + +import Data.Kind +import Type.Reflection + +pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a +pattern Is <- (eqTypeRep (typeRep @b) -> Just HRefl) + where Is = typeRep + +def :: TypeRep a -> a +def x = case x of + Is @Int -> 10 + Is @Bool -> False diff --git a/testsuite/tests/gadt/T19847a.hs b/testsuite/tests/gadt/T19847a.hs new file mode 100644 index 0000000000..a1539d9b06 --- /dev/null +++ b/testsuite/tests/gadt/T19847a.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE LambdaCase, GADTs, ScopedTypeVariables, TypeAbstractions #-} + +module T19847a where + +data T a b c where + MkT :: forall c y x b. (x~y, c~[x], Ord x) => x -> y -> T (x,y) b c + +f :: forall b c. (T (Int,Int) b c -> Bool) -> (b,c) +f = error "urk" + +h = f (\case { MkT @_ @_ @_ @Int p q -> True }) +-- Check that the @Int argument can affect +-- the type at which `f` is instantiated +-- So h :: forall c. (Int,c) diff --git a/testsuite/tests/gadt/T19847a.stderr b/testsuite/tests/gadt/T19847a.stderr new file mode 100644 index 0000000000..1505303835 --- /dev/null +++ b/testsuite/tests/gadt/T19847a.stderr @@ -0,0 +1,12 @@ +TYPE SIGNATURES + f :: forall b c. (T (Int, Int) b c -> Bool) -> (b, c) + h :: forall {c}. (Int, c) +TYPE CONSTRUCTORS + data type T{4} :: forall {k}. * -> k -> * -> * + roles nominal nominal phantom nominal +DATA CONSTRUCTORS + MkT :: forall {k} c y x (b :: k). + (x ~ y, c ~ [x], Ord x) => + x -> y -> T (x, y) b c +Dependent modules: [] +Dependent packages: [base-4.18.0.0] diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T index 1b32762525..39db360e89 100644 --- a/testsuite/tests/gadt/all.T +++ b/testsuite/tests/gadt/all.T @@ -126,3 +126,5 @@ test('SynDataRec', normal, compile, ['']) test('T20485', normal, compile, ['']) test('T20485a', normal, compile, ['']) test('T22235', normal, compile, ['']) +test('T19847', normal, compile, ['']) +test('T19847a', normal, compile, ['-ddump-types']) diff --git a/testsuite/tests/typecheck/should_compile/T19577.hs b/testsuite/tests/typecheck/should_compile/T19577.hs new file mode 100644 index 0000000000..5ec90ca3a0 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T19577.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} + +module T19577 where + +data SBool (b :: Bool) where + STrue :: forall b. (b ~ 'True) => SBool b + SFalse :: forall b. (b ~ 'False) => SBool b + +class Blah b where + blah :: SBool b + +instance Blah 'True where + blah = STrue + +foo :: Blah b => (SBool b -> Int) -> Int +foo f = f blah + +bar = foo (\(STrue @True) -> 42) diff --git a/testsuite/tests/typecheck/should_compile/T21501.hs b/testsuite/tests/typecheck/should_compile/T21501.hs new file mode 100644 index 0000000000..b5990557b3 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T21501.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE MonoLocalBinds, PatternSynonyms, ViewPatterns, TypeAbstractions #-} + +module T21501 where + +import Data.Kind +import Type.Reflection + +pattern TypeApp :: + forall {k1} {k2} (f :: k1 -> k2) (result :: k2). + Typeable f => + forall (arg :: k1). + result ~ f arg => + TypeRep arg -> + TypeRep result +pattern TypeApp arg_rep <- App (eqTypeRep (typeRep @f) -> Just HRefl) arg_rep + +f :: TypeRep (a :: Type) -> String +f (TypeApp @[] rep) = show rep + +{- Expected type: TypeRep k (a::k) + Instantiate at k10 k20 (f0 :: k10 -> k20) (result0 :: k20) + Unify (TypeRep k (a::k) ~ TypeRep k20 (result :: k20) + Unify f0 ~ [] +-} diff --git a/testsuite/tests/typecheck/should_compile/T22383.hs b/testsuite/tests/typecheck/should_compile/T22383.hs new file mode 100644 index 0000000000..7a61c8508b --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22383.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase, ScopedTypeVariables #-} + +module T22383 where + +import Data.Kind (Type) +import Data.Proxy (Proxy(Proxy)) + +-- | @IsType k@ witnesses that @k ~ Type at . +data IsType k where + IsType :: IsType Type + +--------------------- +-- Using a GADT +--------------------- + +data FromType where + FromType :: forall (f :: Type -> Type). FromType + +-- | @FunRep (f b)@ witnesses that @b :: Type at . +data FunRep a where + AppK :: + forall (k :: Type) (f :: k -> Type) (b :: k). + IsType k -> + Proxy f -> + FunRep (f b) + +-- Could not deduce: k ~ * +isMaybeF :: forall (a :: Type). FunRep a -> FromType +isMaybeF = \case + AppK @_ @f @_ t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType @f + +-- Could not deduce: k ~ * +isMaybeG :: forall (a :: Type). FunRep a -> FromType +isMaybeG = \case + AppK @_ @f @_ t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType @g + +-- Works fine +isMaybeH :: forall (a :: Type). FunRep a -> FromType +isMaybeH = \case + AppK @_ @f @_ t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType @h + + +--------------------- +-- Not using a GADT +--------------------- + +data FunRep2 a where + AppK2 :: + forall k (b :: k). + IsType k -> + Proxy k -> + FunRep2 b + +data FromType2 where + FromType2 :: forall (b :: Type). FromType2 + +-- Could not deduce: k ~ * +isMaybeF2 :: forall k (a :: k). FunRep2 a -> FromType2 +isMaybeF2 = \case + AppK2 @_ @f t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType2 @f + +-- Works fine +isMaybeG2 :: forall k (a :: k). FunRep2 a -> FromType2 +isMaybeG2 = \case + AppK2 @_ @f t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType2 @g + +-- Works fine +isMaybeH2 :: forall k (a :: k). FunRep2 a -> FromType2 +isMaybeH2 = \case + AppK2 @_ @f t (Proxy @g :: Proxy h) -> + case t of + IsType -> FromType2 @h diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 5250676032..bbf868fa42 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -856,3 +856,6 @@ test('T22310', normal, compile, ['']) test('T22331', normal, compile, ['']) test('T22516', normal, compile, ['']) test('T22647', normal, compile, ['']) +test('T19577', normal, compile, ['']) +test('T22383', normal, compile, ['']) +test('T21501', normal, compile, ['']) |