diff options
| -rw-r--r-- | compiler/coreSyn/CoreLint.hs | 6 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreOpt.hs | 35 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreSyn.hs | 71 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreUtils.hs | 18 | ||||
| -rw-r--r-- | compiler/coreSyn/MkCore.hs | 4 | ||||
| -rw-r--r-- | compiler/simplCore/Simplify.hs | 26 | ||||
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 74 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 9 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 13 | ||||
| -rw-r--r-- | testsuite/tests/quantified-constraints/T15359.hs | 12 | ||||
| -rw-r--r-- | testsuite/tests/quantified-constraints/T15359a.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/quantified-constraints/T15625.hs | 16 | ||||
| -rw-r--r-- | testsuite/tests/quantified-constraints/T15625a.hs | 20 | ||||
| -rw-r--r-- | testsuite/tests/quantified-constraints/all.T | 4 |
14 files changed, 249 insertions, 73 deletions
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 6dee383cd9..349d36d8e2 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -519,6 +519,11 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs) ; binder_ty <- applySubstTy (idType binder) ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty) + -- If the binding is for a CoVar, the RHS should be (Coercion co) + -- See Note [CoreSyn type and coercion invariant] in CoreSyn + ; checkL (not (isCoVar binder) || isCoArg rhs) + (mkLetErr binder rhs) + -- Check that it's not levity-polymorphic -- Do this first, because otherwise isUnliftedType panics -- Annoyingly, this duplicates the test in lintIdBdr, @@ -842,6 +847,7 @@ lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed lintVarOcc var nargs = do { checkL (isNonCoVarId var) (text "Non term variable" <+> ppr var) + -- See CoreSyn Note [Variable occurrences in Core] -- Cneck that the type of the occurrence is the same -- as the type of the binding site diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 8a41c98822..3254d7334c 100644 --- a/compiler/coreSyn/CoreOpt.hs +++ b/compiler/coreSyn/CoreOpt.hs @@ -32,7 +32,7 @@ import PprCore ( pprCoreBindings, pprRules ) import OccurAnal( occurAnalyseExpr, occurAnalysePgm ) import Literal ( Literal(MachStr) ) import Id -import Var ( varType ) +import Var ( varType, isNonCoVarId ) import VarSet import VarEnv import DataCon @@ -360,7 +360,10 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst }) = ASSERT( isCoVar in_bndr ) (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing) - | pre_inline_unconditionally + | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr ) + -- The previous two guards got rid of tyvars and coercions + -- See Note [CoreSyn type and coercion invariant] in CoreSyn + pre_inline_unconditionally = (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing) | otherwise @@ -385,12 +388,11 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst }) pre_inline_unconditionally :: Bool pre_inline_unconditionally - | isCoVar in_bndr = False -- See Note [Do not inline CoVars unconditionally] - | isExportedId in_bndr = False -- in SimplUtils + | isExportedId in_bndr = False | stable_unf = False | not active = False -- Note [Inline prag in simplOpt] | not (safe_to_inline occ) = False - | otherwise = True + | otherwise = True -- Unconditionally safe to inline safe_to_inline :: OccInfo -> Bool @@ -423,7 +425,10 @@ simple_out_bind_pair :: SimpleOptEnv -> (SimpleOptEnv, Maybe (OutVar, OutExpr)) simple_out_bind_pair env in_bndr mb_out_bndr out_rhs occ_info active stable_unf - | post_inline_unconditionally + | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr ) + -- Type and coercion bindings are caught earlier + -- See Note [CoreSyn type and coercion invariant] + post_inline_unconditionally = ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs } , Nothing) @@ -437,14 +442,16 @@ simple_out_bind_pair env in_bndr mb_out_bndr out_rhs post_inline_unconditionally :: Bool post_inline_unconditionally - | not active = False - | isWeakLoopBreaker occ_info = False -- If it's a loop-breaker of any kind, don't inline - -- because it might be referred to "earlier" - | stable_unf = False -- Note [Stable unfoldings and postInlineUnconditionally] - | isExportedId in_bndr = False -- Note [Exported Ids and trivial RHSs] - | exprIsTrivial out_rhs = True - | coercible_hack = True - | otherwise = False + | isExportedId in_bndr = False -- Note [Exported Ids and trivial RHSs] + | stable_unf = False -- Note [Stable unfoldings and postInlineUnconditionally] + | not active = False -- in SimplUtils + | is_loop_breaker = False -- If it's a loop-breaker of any kind, don't inline + -- because it might be referred to "earlier" + | exprIsTrivial out_rhs = True + | coercible_hack = True + | otherwise = False + + is_loop_breaker = isWeakLoopBreaker occ_info -- See Note [Getting the map/coerce RULE to work] coercible_hack | (Var fun, args) <- collectArgs out_rhs diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs index 025c19e3ca..aa27d7a7fb 100644 --- a/compiler/coreSyn/CoreSyn.hs +++ b/compiler/coreSyn/CoreSyn.hs @@ -46,7 +46,7 @@ module CoreSyn ( exprToType, exprToCoercion_maybe, applyTypeToArg, - isValArg, isTypeArg, isTyCoArg, valArgCount, valBndrCount, + isValArg, isTypeArg, isCoArg, isTyCoArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar, -- * Tick-related functions @@ -173,6 +173,7 @@ These data types are the heart of the compiler -- The language consists of the following elements: -- -- * Variables +-- See Note [Variable occurrences in Core] -- -- * Primitive literals -- @@ -187,29 +188,10 @@ These data types are the heart of the compiler -- this corresponds to allocating a thunk for the things -- bound and then executing the sub-expression. -- --- #top_level_invariant# --- #letrec_invariant# --- --- The right hand sides of all top-level and recursive @let@s --- /must/ be of lifted type (see "Type#type_classification" for --- the meaning of /lifted/ vs. /unlifted/). There is one exception --- to this rule, top-level @let@s are allowed to bind primitive --- string literals, see Note [CoreSyn top-level string literals]. --- +-- See Note [CoreSyn letrec invariant] -- See Note [CoreSyn let/app invariant] -- See Note [Levity polymorphism invariants] --- --- #type_let# --- We allow a /non-recursive/ let to bind a type variable, thus: --- --- > Let (NonRec tv (Type ty)) body --- --- This can be very convenient for postponing type substitutions until --- the next run of the simplifier. --- --- At the moment, the rest of the compiler only deals with type-let --- in a Let expression, rather than at top level. We may want to revist --- this choice. +-- See Note [CoreSyn type and coercion invariant] -- -- * Case expression. Operationally this corresponds to evaluating -- the scrutinee (expression examined) to weak head normal form @@ -371,13 +353,25 @@ PrelRules for the rationale for this restriction. -------------------------- CoreSyn INVARIANTS --------------------------- -Note [CoreSyn top-level invariant] +Note [Variable occurrences in Core] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See #toplevel_invariant# +Variable /occurrences/ are never CoVars, though /bindings/ can be. +All CoVars appear in Coercions. + +For example + \(c :: Age~#Int) (d::Int). d |> (sym c) +Here 'c' is a CoVar, which is lambda-bound, but it /occurs/ in +a Coercion, (sym c). Note [CoreSyn letrec invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See #letrec_invariant# +The right hand sides of all top-level and recursive @let@s +/must/ be of lifted type (see "Type#type_classification" for +the meaning of /lifted/ vs. /unlifted/). + +There is one exception to this rule, top-level @let@s are +allowed to bind primitive string literals: see +Note [CoreSyn top-level string literals]. Note [CoreSyn top-level string literals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -451,6 +445,27 @@ which will generate a @case@ if necessary The let/app invariant is initially enforced by mkCoreLet and mkCoreApp in coreSyn/MkCore. +Note [CoreSyn type and coercion invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We allow a /non-recursive/, /non-top-level/ let to bind type and +coercion variables. These can be very convenient for postponing type +substitutions until the next run of the simplifier. + +* A type variable binding must have a RHS of (Type ty) + +* A coercion variable binding must have a RHS of (Coercion co) + + It is possible to have terms that return a coercion, but we use + case-binding for those; e.g. + case (eq_sel d) of (co :: a ~# b) -> blah + where eq_sel :: (a~b) -> (a~#b) + + Or even even + case (df @Int) of (co :: a ~# b) -> blah + Which is very exotic, and I think never encountered; but see + Note [Equality superclasses in quantified constraints] + in TcCanonical + Note [CoreSyn case invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See #case_invariants# @@ -2102,6 +2117,12 @@ isTyCoArg (Type {}) = True isTyCoArg (Coercion {}) = True isTyCoArg _ = False +-- | Returns @True@ iff the expression is a 'Coercion' +-- expression at its top level +isCoArg :: Expr b -> Bool +isCoArg (Coercion {}) = True +isCoArg _ = False + -- | Returns @True@ iff the expression is a 'Type' expression at its -- top level. Note this does NOT include 'Coercion's. isTypeArg :: Expr b -> Bool diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs index 3c65072974..7635a6d66a 100644 --- a/compiler/coreSyn/CoreUtils.hs +++ b/compiler/coreSyn/CoreUtils.hs @@ -481,8 +481,15 @@ bindNonRec :: Id -> CoreExpr -> CoreExpr -> CoreExpr -- the simplifier deals with them perfectly well. See -- also 'MkCore.mkCoreLet' bindNonRec bndr rhs body - | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT, [], body)] - | otherwise = Let (NonRec bndr rhs) body + | isTyVar bndr = let_bind + | isCoVar bndr = if isCoArg rhs then let_bind + {- See Note [Binding coercions] -} else case_bind + | isJoinId bndr = let_bind + | needsCaseBinding (idType bndr) rhs = case_bind + | otherwise = let_bind + where + case_bind = Case rhs bndr (exprType body) [(DEFAULT, [], body)] + let_bind = Let (NonRec bndr rhs) body -- | Tests whether we have to use a @case@ rather than @let@ binding for this expression -- as per the invariants of 'CoreExpr': see "CoreSyn#let_app_invariant" @@ -505,7 +512,12 @@ mkAltExpr (LitAlt lit) [] [] mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt" mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT" -{- +{- Note [Binding coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider binding a CoVar, c = e. Then, we must atisfy +Note [CoreSyn type and coercion invariant] in CoreSyn, +which allows only (Coercion co) on the RHS. + ************************************************************************ * * Operations oer case alternatives diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index c3b1625333..a425ad249e 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -107,9 +107,7 @@ sortQuantVars vs = sorted_tcvs ++ ids -- appropriate (see "CoreSyn#let_app_invariant") mkCoreLet :: CoreBind -> CoreExpr -> CoreExpr mkCoreLet (NonRec bndr rhs) body -- See Note [CoreSyn let/app invariant] - | needsCaseBinding (idType bndr) rhs - , not (isJoinId bndr) - = Case rhs bndr (exprType body) [(DEFAULT,[],body)] + = bindNonRec bndr rhs body mkCoreLet bind body = Let bind body diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs index 1041bc13cc..872973925f 100644 --- a/compiler/simplCore/Simplify.hs +++ b/compiler/simplCore/Simplify.hs @@ -44,6 +44,7 @@ import Demand ( mkClosedStrictSig, topDmd, exnRes ) import BasicTypes ( TopLevelFlag(..), isNotTopLevel, isTopLevel, RecFlag(..), Arity ) import MonadUtils ( mapAccumLM, liftIO ) +import Var ( isTyCoVar ) import Maybes ( orElse ) import Control.Monad import Outputable @@ -2425,9 +2426,7 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont -- lifted case: the scrutinee is in HNF (or will later be demanded) -- See Note [Case to let transformation] | all_dead_bndrs - , if isUnliftedType (idType case_bndr) - then exprOkForSpeculation scrut - else exprIsHNF scrut || case_bndr_is_demanded + , doCaseToLet scrut case_bndr = do { tick (CaseElim case_bndr) ; (floats1, env') <- simplNonRecX env case_bndr scrut ; (floats2, expr') <- simplExprF env' rhs cont @@ -2446,12 +2445,27 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont all_dead_bndrs = all isDeadBinder bndrs -- bndrs are [InId] is_plain_seq = all_dead_bndrs && isDeadBinder case_bndr -- Evaluation *only* for effect - case_bndr_is_demanded = isStrictDmd (idDemandInfo case_bndr) - -- See Note [Case-to-let for strictly-used binders] - rebuildCase env scrut case_bndr alts cont = reallyRebuildCase env scrut case_bndr alts cont + +doCaseToLet :: OutExpr -- Scrutinee + -> InId -- Case binder + -> Bool +-- The situation is case scrut of b { DEFAULT -> body } +-- Can we transform thus? let { b = scrut } in body +doCaseToLet scrut case_bndr + | isTyCoVar case_bndr -- Respect CoreSyn + = isTyCoArg scrut -- Note [CoreSyn type and coercion invariant] + + | isUnliftedType (idType case_bndr) + = exprOkForSpeculation scrut + + | otherwise -- Scrut has a lifted type + = exprIsHNF scrut + || isStrictDmd (idDemandInfo case_bndr) + -- See Note [Case-to-let for strictly-used binders] + -------------------------------------------------- -- 3. Catch-all case -------------------------------------------------- diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index b9b59d121f..3ff54dff5c 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -23,6 +23,7 @@ import TcEvTerm import Class import TyCon import TyCoRep -- cleverly decomposes types, good for completeness checking +import TysWiredIn( cTupleTyConName ) import Coercion import CoreSyn import Id( idType, mkTemplateLocals ) @@ -487,16 +488,31 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys size = sizeTypes tys do_one_given evar given_loc sel_id - = do { let sc_pred = funResultTy (piResultTys (idType sel_id) tys) - given_ty = mkInfSigmaTy tvs theta sc_pred - ; given_ev <- newGivenEvVar given_loc $ - (given_ty, mk_sc_sel evar sel_id) + | not (null tvs) + , null theta + , isUnliftedType sc_pred + -- Very special case for equality + -- See Note [Equality superclasses in quantified constraints] + = do { empty_ctuple_cls <- tcLookupClass (cTupleTyConName 0) + ; let theta1 = [mkClassPred empty_ctuple_cls []] + dict_ids1 = mkTemplateLocals theta1 + ; given_ev <- new_given theta1 dict_ids1 [] + ; return [mkNonCanonical given_ev] } + + | otherwise -- Normal case + = do { given_ev <- new_given theta dict_ids dict_ids ; mk_superclasses rec_clss given_ev tvs theta sc_pred } - mk_sc_sel evar sel_id - = EvExpr $ mkLams tvs $ mkLams dict_ids $ - Var sel_id `mkTyApps` tys `App` - (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids) + where + sc_pred = funResultTy (piResultTys (idType sel_id) tys) + + new_given theta_abs dict_ids_abs dict_ids_app + = newGivenEvVar given_loc (given_ty, given_ev) + where + given_ty = mkInfSigmaTy tvs theta_abs sc_pred + given_ev = EvExpr $ mkLams tvs $ mkLams dict_ids_abs $ + Var sel_id `mkTyApps` tys `App` + (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids_app) mk_given_loc loc | isCTupleClass cls @@ -574,7 +590,45 @@ mk_superclasses_of rec_clss ev tvs theta cls tys , qci_pend_sc = loop_found }) -{- +{- Note [Equality superclasses in quantified constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (Trac #15359, #15593, #15625) + f :: (forall a. theta => a ~ b) => stuff + +It's a bit odd to have a local, quantified constraint for `(a~b)`, +but some people want such a thing (see the tickets). And for +Coercible it is definitely useful + f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))) + => stuff + +Moreover it's not hard to arrange; we just need to look up /equality/ +constraints in the quantified-constraint environment, which we do in +TcInteract.doTopReactOther. + +There is a wrinkle though, in the case where 'theta' is empty, so +we have + f :: (forall a. a~b) => stuff + +Now the superclass machinery kicks in, in makeSuperClasses, +giving us a a second quantified constrait + (forall a. a ~# b) +BUT this is an unboxed value! And nothing has prepared us for +dictionary "functions" that are unboxed. Actually it does just +about work, but the simplier ends up with stuff like + case (/\a. eq_sel d) of df -> ...(df @Int)... +and fails to simplify that any further. + +It seems eaiser to give such unboxed quantifed constraints a +dummmy () argument, thus + (forall a. (% %) => a ~# b) +where (% %) is the empty constraint tuple. That makes everything +be nicely boxed. + +(One might wonder about using void# instead, but this seems more +uniform -- it's a constraint argument -- and I'm not worried about +the last drop of efficiency for this very rare case.) + + ************************************************************************ * * * Irreducibles canonicalization @@ -2013,7 +2067,7 @@ canEqTyVarTyVar, are these gets eliminated (improves error messages) * If one is a flatten-skolem, put it on the left so that it is - substituted out Note [Elminate flat-skols] + substituted out Note [Eliminate flat-skols] in TcUinfy fsk ~ a Note [Equalities with incompatible kinds] diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 028b755187..1771e19849 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1820,9 +1820,14 @@ topReactionsStage work_item -------------------- doTopReactOther :: Ct -> TcS (StopOrContinue Ct) +-- Try local quantified constraints for +-- CTyEqCan e.g. (a ~# ty) +-- and CIrredCan e.g. (c a) +-- +-- Why equalities? See TcCanonical +-- Note [Equality superclasses in quantified constraints] doTopReactOther work_item - = do { -- Try local quantified constraints - res <- matchLocalInst pred (ctEvLoc ev) + = do { res <- matchLocalInst pred (ctEvLoc ev) ; case res of OneInst {} -> chooseInstance work_item res _ -> continueWith work_item } diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 2fde421f79..b58c1ba74e 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1142,21 +1142,14 @@ check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args , hand_written_bindings = failWithTc rejected_class_msg - -- For the most part we don't allow instances for Coercible; + -- For the most part we don't allow + -- instances for (~), (~~), or Coercible; -- but we DO want to allow them in quantified constraints: -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m... - | clas_nm == coercibleTyConName + | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ] , not quantified_constraint = failWithTc rejected_class_msg - -- Handwritten instances of other nonminal-equality classes - -- is forbidden, except in the defining module to allow - -- instance a ~~ b => a ~ b - -- which occurs in Data.Type.Equality - | clas_nm `elem` [ heqTyConName, eqTyConName] - , nameModule clas_nm /= this_mod - = failWithTc rejected_class_msg - -- Check for hand-written Generic instances (disallowed in Safe Haskell) | clas_nm `elem` genericClassNames , hand_written_bindings diff --git a/testsuite/tests/quantified-constraints/T15359.hs b/testsuite/tests/quantified-constraints/T15359.hs new file mode 100644 index 0000000000..7ef1cc5572 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15359.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes, + ConstraintKinds, QuantifiedConstraints #-} + +module T15359 where + +class C a b + +data Dict c where + Dict :: c => Dict c + +foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b +foo Dict x = x diff --git a/testsuite/tests/quantified-constraints/T15359a.hs b/testsuite/tests/quantified-constraints/T15359a.hs new file mode 100644 index 0000000000..6ec5f861a8 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15359a.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes, + ConstraintKinds, QuantifiedConstraints, + UndecidableInstances #-} + +module T15359a where + +class C a b +class a ~ b => D a b + +data Dict c where + Dict :: c => Dict c + +foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b +foo Dict x = x diff --git a/testsuite/tests/quantified-constraints/T15625.hs b/testsuite/tests/quantified-constraints/T15625.hs new file mode 100644 index 0000000000..8fe092da98 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15625.hs @@ -0,0 +1,16 @@ +{-# Language GADTs, MultiParamTypeClasses, QuantifiedConstraints #-} + +module T15625 where + +import Data.Coerce + +class a ~ b => Equal a b + +test1 :: (forall b. a ~ b) => a +test1 = False + +test2 :: (forall b. Equal a b) => a +test2 = False + +test3 :: (forall b. Coercible a b) => a +test3 = coerce False diff --git a/testsuite/tests/quantified-constraints/T15625a.hs b/testsuite/tests/quantified-constraints/T15625a.hs new file mode 100644 index 0000000000..ca049cb19d --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15625a.hs @@ -0,0 +1,20 @@ +{-# Language RankNTypes, ConstraintKinds, QuantifiedConstraints, + PolyKinds, GADTs, MultiParamTypeClasses, + DataKinds, FlexibleInstances #-} + +module T15625a where + +import Data.Kind + +type Cat ob = ob -> ob -> Type + +data KLEISLI (m :: Type -> Type) :: Cat (KL_kind m) where + MkKLEISLI :: (a -> m b) -> KLEISLI(m) (KL a) (KL b) + +data KL_kind (m :: Type -> Type) = KL Type + +class (a ~ KL xx) => AsKL a xx +instance (a ~ KL xx) => AsKL a xx + +ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a +ekki__ = MkKLEISLI undefined diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T index 833a667ea9..1e2eca8358 100644 --- a/testsuite/tests/quantified-constraints/all.T +++ b/testsuite/tests/quantified-constraints/all.T @@ -16,3 +16,7 @@ test('T15290a', normal, compile_fail, ['']) test('T15290b', normal, compile_fail, ['']) test('T15316', normal, compile_fail, ['']) test('T15334', normal, compile_fail, ['']) +test('T15359', normal, compile, ['']) +test('T15359a', normal, compile, ['']) +test('T15625', normal, compile, ['']) +test('T15625a', normal, compile, ['']) |