Commit bd76875a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow (~) in the head of a quantified constraints

Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
  f :: (forall a. blah => a ~ ty) => stuff

I am frankly dubious that this is ever useful.  But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well.  Plus, our users are asking for it
(Trac #15359, #15625).

It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]

There are a number of wrinkles:

* If the context of the quantified constraint is empty, we
  can get trouble when we get down to unboxed equality (a ~# b)
  or (a ~R# b), as Trac #15625 showed. This is even more of
  a corner case, but it produced an outright crash, so I elaborated
  the superclass machinery in TcCanonical.makeStrictSuperClasses
  to add a void argument in this case.  See
  Note [Equality superclasses in quantified constraints]

* The restriction on (~) was in TcValidity.checkValidInstHead.
  In lifting the restriction I discovered an old special case for
  (~), namely
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      , nameModule clas_nm /= this_mod
  This was (solely) to support the strange instance
      instance a ~~ b => a ~ b
  in Data.Type.Equality. But happily that is no longer
  with us, since
     commit f265008f
     Refactor (~) to reduce the suerpclass stack
  So I removed the special case.

* I found that the Core invariants on when we could have
       co = <expr>
  were entirely not written down. (Getting this wrong ws
  the proximate source of the crash in Trac #15625.  So

  - Documented them better in CoreSyn
      Note [CoreSyn type and coercion invariant],
  - Modified CoreOpt and CoreLint to match
  - Modified CoreUtils.bindNonRec to match
  - Made MkCore.mkCoreLet use bindNonRec, rather
    than duplicate its logic
  - Made Simplify.rebuildCase case-to-let respect
      Note [CoreSyn type and coercion invariant],
parent 291b0f89
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
--------------------------------------------------
......
......@@ -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]
......
......@@ -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 }
......
......@@ -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
......
{-# 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
{-# 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
{-# 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
{-# 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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment