summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKrzysztof Gogolewski <krzysztof.gogolewski@tweag.io>2022-05-14 01:07:36 +0200
committerKrzysztof Gogolewski <krzysztof.gogolewski@tweag.io>2022-05-27 16:44:48 +0200
commit3bd7d5d668b316f517a66c72fcf9bc7a36cc6ba4 (patch)
tree186c133c0259d87f04b79c2017b7ee858b1b380a
parented37027f713bb6563fd98d144a39211339fd91a5 (diff)
downloadhaskell-3bd7d5d668b316f517a66c72fcf9bc7a36cc6ba4.tar.gz
Use a class to check validity of withDictwip/withdict
This moves handling of the magic 'withDict' function from the desugarer to the typechecker. Details in Note [withDict]. I've extracted a part of T16646Fail to a separate file T16646Fail2, because the new error in 'reify' hides the errors from 'f' and 'g'. WithDict now works with casts, this fixes #21328. Part of #19915
-rw-r--r--compiler/GHC/Builtin/Names.hs17
-rw-r--r--compiler/GHC/HsToCore/Errors/Ppr.hs8
-rw-r--r--compiler/GHC/HsToCore/Errors/Types.hs2
-rw-r--r--compiler/GHC/HsToCore/Expr.hs193
-rw-r--r--compiler/GHC/Tc/Instance/Class.hs180
-rw-r--r--compiler/GHC/Tc/Validity.hs2
-rw-r--r--libraries/base/Data/Typeable/Internal.hs2
-rwxr-xr-xlibraries/base/GHC/Exts.hs2
-rw-r--r--libraries/base/GHC/TypeLits.hs8
-rw-r--r--libraries/base/GHC/TypeNats.hs8
-rw-r--r--libraries/ghc-prim/GHC/Magic/Dict.hs14
-rw-r--r--libraries/ghc-prim/changelog.md7
-rw-r--r--testsuite/tests/ghci/scripts/T19667Ghci.hs2
-rw-r--r--testsuite/tests/simplCore/should_run/T21575.hs6
-rw-r--r--testsuite/tests/typecheck/should_compile/T21328.hs17
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T1
-rw-r--r--testsuite/tests/typecheck/should_fail/T16646Fail.hs12
-rw-r--r--testsuite/tests/typecheck/should_fail/T16646Fail.stderr18
-rw-r--r--testsuite/tests/typecheck/should_fail/T16646Fail2.hs19
-rw-r--r--testsuite/tests/typecheck/should_fail/T16646Fail2.stderr16
-rw-r--r--testsuite/tests/typecheck/should_fail/T19915.hs5
-rw-r--r--testsuite/tests/typecheck/should_fail/T19915.stderr4
-rw-r--r--testsuite/tests/typecheck/should_fail/T21328.hs11
-rw-r--r--testsuite/tests/typecheck/should_fail/T21328.stderr4
-rw-r--r--testsuite/tests/typecheck/should_fail/all.T3
-rw-r--r--testsuite/tests/typecheck/should_run/T16646.hs8
-rw-r--r--testsuite/tests/typecheck/should_run/T19667.hs2
27 files changed, 299 insertions, 272 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index e99cb5a1c6..8aad951de0 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -222,7 +222,6 @@ basicKnownKeyNames
ioTyConName, ioDataConName,
runMainIOName,
runRWName,
- withDictName,
-- Type representation types
trModuleTyConName, trModuleDataConName,
@@ -259,6 +258,9 @@ basicKnownKeyNames
starArrStarKindRepName,
starArrStarArrStarKindRepName,
+ -- WithDict
+ withDictClassName,
+
-- Dynamic
toDynName,
@@ -931,10 +933,9 @@ and it's convenient to write them all down in one place.
wildCardName :: Name
wildCardName = mkSystemVarName wildCardKey (fsLit "wild")
-runMainIOName, runRWName, withDictName :: Name
+runMainIOName, runRWName :: Name
runMainIOName = varQual gHC_TOP_HANDLER (fsLit "runMainIO") runMainKey
runRWName = varQual gHC_MAGIC (fsLit "runRW#") runRWKey
-withDictName = varQual gHC_MAGIC_DICT (fsLit "withDict") withDictKey
orderingTyConName, ordLTDataConName, ordEQDataConName, ordGTDataConName :: Name
orderingTyConName = tcQual gHC_TYPES (fsLit "Ordering") orderingTyConKey
@@ -1403,6 +1404,10 @@ starKindRepName = varQual gHC_TYPES (fsLit "krep$*") star
starArrStarKindRepName = varQual gHC_TYPES (fsLit "krep$*Arr*") starArrStarKindRepKey
starArrStarArrStarKindRepName = varQual gHC_TYPES (fsLit "krep$*->*->*") starArrStarArrStarKindRepKey
+-- WithDict
+withDictClassName :: Name
+withDictClassName = clsQual gHC_MAGIC_DICT (fsLit "WithDict") withDictClassKey
+
-- Custom type errors
errorMessageTypeErrorFamName
, typeErrorTextDataConName
@@ -1707,6 +1712,9 @@ ixClassKey = mkPreludeClassUnique 18
typeableClassKey :: Unique
typeableClassKey = mkPreludeClassUnique 20
+withDictClassKey :: Unique
+withDictClassKey = mkPreludeClassUnique 21
+
monadFixClassKey :: Unique
monadFixClassKey = mkPreludeClassUnique 28
@@ -2343,9 +2351,6 @@ rationalToFloatIdKey, rationalToDoubleIdKey :: Unique
rationalToFloatIdKey = mkPreludeMiscIdUnique 132
rationalToDoubleIdKey = mkPreludeMiscIdUnique 133
-withDictKey :: Unique
-withDictKey = mkPreludeMiscIdUnique 156
-
coerceKey :: Unique
coerceKey = mkPreludeMiscIdUnique 157
diff --git a/compiler/GHC/HsToCore/Errors/Ppr.hs b/compiler/GHC/HsToCore/Errors/Ppr.hs
index a1aa921b2e..9695eee60c 100644
--- a/compiler/GHC/HsToCore/Errors/Ppr.hs
+++ b/compiler/GHC/HsToCore/Errors/Ppr.hs
@@ -3,7 +3,6 @@
module GHC.HsToCore.Errors.Ppr where
-import GHC.Builtin.Names (withDictName)
import GHC.Core.Predicate (isEvVar)
import GHC.Core.Type
import GHC.Driver.Flags
@@ -181,11 +180,6 @@ instance Diagnostic DsMessage where
-> mkSimpleDecorated $
hang (text "You can't mix polymorphic and unlifted bindings:")
2 (ppr bind)
- DsInvalidInstantiationDictAtType wrapped_ty
- -> mkSimpleDecorated $
- hang (text "Invalid instantiation of" <+>
- quotes (ppr withDictName) <+> text "at type:")
- 4 (ppr wrapped_ty)
DsWrongDoBind _rhs elt_ty
-> mkSimpleDecorated $ badMonadBind elt_ty
DsUnusedDoBind _rhs elt_ty
@@ -235,7 +229,6 @@ instance Diagnostic DsMessage where
DsAggregatedViewExpressions{} -> WarningWithoutFlag
DsUnbangedStrictPatterns{} -> WarningWithFlag Opt_WarnUnbangedStrictPatterns
DsCannotMixPolyAndUnliftedBindings{} -> ErrorWithoutFlag
- DsInvalidInstantiationDictAtType{} -> ErrorWithoutFlag
DsWrongDoBind{} -> WarningWithFlag Opt_WarnWrongDoBind
DsUnusedDoBind{} -> WarningWithFlag Opt_WarnUnusedDoBind
DsRecBindsNotAllowedForUnliftedTys{} -> ErrorWithoutFlag
@@ -276,7 +269,6 @@ instance Diagnostic DsMessage where
DsWrongDoBind rhs _ -> [SuggestBindToWildcard rhs]
DsUnusedDoBind rhs _ -> [SuggestBindToWildcard rhs]
DsRecBindsNotAllowedForUnliftedTys{} -> noHints
- DsInvalidInstantiationDictAtType{} -> noHints
DsRuleMightInlineFirst _ lhs_id rule_act -> [SuggestAddInlineOrNoInlinePragma lhs_id rule_act]
DsAnotherRuleMightFireFirst _ bad_rule _ -> [SuggestAddPhaseToCompetingRule bad_rule]
diff --git a/compiler/GHC/HsToCore/Errors/Types.hs b/compiler/GHC/HsToCore/Errors/Types.hs
index 55164e741b..d178eecfed 100644
--- a/compiler/GHC/HsToCore/Errors/Types.hs
+++ b/compiler/GHC/HsToCore/Errors/Types.hs
@@ -134,8 +134,6 @@ data DsMessage
| DsCannotMixPolyAndUnliftedBindings !(HsBindLR GhcTc GhcTc)
- | DsInvalidInstantiationDictAtType !Type
-
| DsWrongDoBind !(LHsExpr GhcTc) !Type
| DsUnusedDoBind !(LHsExpr GhcTc) !Type
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index bc287f433c..84dd992037 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -43,7 +43,6 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad
import GHC.Core.Type
import GHC.Core.TyCo.Rep
-import GHC.Core.Coercion( instNewTyCon_maybe, mkSymCo )
import GHC.Core
import GHC.Core.Utils
import GHC.Core.Make
@@ -757,8 +756,6 @@ dsDo ctx stmts
dsHsVar :: Id -> DsM CoreExpr
-- We could just call dsHsUnwrapped; but this is a short-cut
-- for the very common case of a variable with no wrapper.
--- NB: withDict is always instantiated by a wrapper, so we need
--- only check for it in dsHsUnwrapped
dsHsVar var
= return (varToCoreExpr var) -- See Note [Desugaring vars]
@@ -831,7 +828,7 @@ warnDiscardedDoBindings rhs rhs_ty
{-
************************************************************************
* *
- dsHsWrapped and ds_withDict
+ dsHsWrapped
* *
************************************************************************
-}
@@ -849,11 +846,6 @@ dsHsWrapped orig_hs_expr
= go (wrap <.> WpTyApp ty) hs_e
go wrap (HsVar _ (L _ var))
- | var `hasKey` withDictKey
- = do { wrap' <- dsHsWrapper wrap
- ; ds_withDict (exprType (wrap' (varToCoreExpr var))) }
-
- | otherwise
= do { wrap' <- dsHsWrapper wrap
; let expr = wrap' (varToCoreExpr var)
ty = exprType expr
@@ -866,186 +858,3 @@ dsHsWrapped orig_hs_expr
; addTyCs FromSource (hsWrapDictBinders wrap) $
do { e <- dsExpr hs_e
; return (wrap' e) } }
-
--- See Note [withDict]
-ds_withDict :: Type -> DsM CoreExpr
-ds_withDict wrapped_ty
- -- Check that withDict is of the type `st -> (dt => r) -> r`.
- | Just (Anon VisArg (Scaled mult1 st), rest) <- splitPiTy_maybe wrapped_ty
- , Just (Anon VisArg (Scaled mult2 dt_to_r), _r1) <- splitPiTy_maybe rest
- , Just (Anon InvisArg (Scaled _ dt), _r2) <- splitPiTy_maybe dt_to_r
- -- Check that dt is a class constraint `C t_1 ... t_n`, where
- -- `dict_tc = C` and `dict_args = t_1 ... t_n`.
- , Just (dict_tc, dict_args) <- splitTyConApp_maybe dt
- -- Check that C is a class of the form
- -- `class C a_1 ... a_n where op :: meth_ty`, where
- -- `meth_tvs = a_1 ... a_n` and `co` is a newtype coercion between
- -- `C` and `meth_ty`.
- , Just (inst_meth_ty, co) <- instNewTyCon_maybe dict_tc dict_args
- -- co :: C t1 ..tn ~R# st
- -- Check that `st` is equal to `meth_ty[t_i/a_i]`.
- , st `eqType` inst_meth_ty
- = do { sv <- newSysLocalDs mult1 st
- ; k <- newSysLocalDs mult2 dt_to_r
- ; let wd_rhs = mkLams [sv, k] $ Var k `App` Cast (Var sv) (mkSymCo co)
- ; wd_id <- newSysLocalDs Many (exprType wd_rhs)
- ; let wd_id' = wd_id `setInlinePragma` inlineAfterSpecialiser
- ; pure $ Let (NonRec wd_id' wd_rhs) (Var wd_id') }
- -- Why a Let? See (WD8) in Note [withDict]
-
- | otherwise
- = errDsCoreExpr (DsInvalidInstantiationDictAtType wrapped_ty)
-
-inlineAfterSpecialiser :: InlinePragma
--- Do not inline before the specialiser; but do so afterwards
--- See (WD8) in Note [withDict]
-inlineAfterSpecialiser = alwaysInlinePragma `setInlinePragmaActivation`
- ActiveAfter NoSourceText 2
-
-{- Note [withDict]
-~~~~~~~~~~~~~~~~~~
-The identifier `withDict` is just a place-holder, which is used to
-implement a primitive that we cannot define in Haskell but we can write
-in Core. It is declared with a place-holder type:
-
- withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
-
-The intention is that the identifier will be used in a very specific way,
-to create dictionaries for classes with a single method. Consider a class
-like this:
-
- class C a where
- f :: T a
-
-We can use `withDict`, in conjunction with a special case in the desugarer, to
-cast values of type `T a` into dictionaries for `C a`. To do this, we can
-define a function like this in the library:
-
- withT :: T a -> (C a => b) -> b
- withT t k = withDict @(T a) @(C a) t k
-
-Here:
-
-* The `dt` in `withDict` (short for "dictionary type") is instantiated to
- `C a`.
-
-* The `st` in `withDict` (short for "singleton type") is instantiated to
- `T a`. The definition of `T` itself is irrelevant, only that `C a` is a class
- with a single method of type `T a`.
-
-* The `r` in `withDict` is instantiated to `b`.
-
-There is a special case in dsHsWrapped.go_head which will replace the RHS
-of this definition with an appropriate definition in Core. The special case
-rewrites applications of `withDict` as follows:
-
- withDict @{rr} @mtype @(C t_1 ... t_n) @r
----->
- \(sv :: mtype) (k :: C t_1 ... t_n => r) -> k (sv |> sym (co t_1 ... t_n))
-
-Where:
-
-* The `C t_1 ... t_n` argument to withDict is a class constraint.
-
-* C must be defined as:
-
- class C a_1 ... a_n where
- op :: meth_type
-
- That is, C must be a class with exactly one method and no superclasses.
-
-* The `mtype` argument to withDict must be equal to `meth_type[t_i/a_i]`,
- which is instantiated type of C's method.
-
-* `co` is a newtype coercion that, when applied to `t_1 ... t_n`, coerces from
- `C t_1 ... t_n` to `mtype`. This coercion is guaranteed to exist by virtue of
- the fact that C is a class with exactly one method and no superclasses, so it
- is treated like a newtype when compiled to Core.
-
-These requirements are implemented in the guards in ds_withDict's definition.
-
-Some further observations about `withDict`:
-
-(WD1) Every use of `withDict` must be instantiated at a /particular/ class C.
- It's a bit like representation polymorphism: we don't allow class-polymorphic
- calls of `withDict`. We check this in the desugarer -- and then we
- can immediately replace this invocation of `withDict` with appropriate
- class-specific Core code.
-
-(WD2) The `dt` in the type of withDict must be explicitly instantiated with
- visible type application, as invoking `withDict` would be ambiguous
- otherwise.
-
- For examples of how `withDict` is used in the `base` library, see `withSNat`
- in GHC.TypeNats, as well as `withSChar` and `withSSymbol` in GHC.TypeLits.
-
-(WD3) The `r` is representation-polymorphic, to support things like
- `withTypeable` in `Data.Typeable.Internal`.
-
-(WD4) As an alternative to `withDict`, one could define functions like `withT`
- above in terms of `unsafeCoerce`. This is more error-prone, however.
-
-(WD5) In order to define things like `reifySymbol` below:
-
- reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
-
- `withDict` needs to be instantiated with `Any`, like so:
-
- reifySymbol n k = withDict @String @(KnownSymbol Any) @r n (k @Any)
-
- The use of `Any` is explained in Note [NOINLINE someNatVal] in
- base:GHC.TypeNats.
-
-(WD6) The only valid way to apply `withDict` is as described above. Applying
- `withDict` in any other way will result in a non-recoverable error during
- desugaring. In other words, GHC will never execute the `withDict` function
- in compiled code.
-
- In theory, this means that we don't need to define a binding for `withDict`
- in GHC.Magic.Dict. In practice, we define a binding anyway, for two reasons:
-
- - To give it Haddocks, and
- - To define the type of `withDict`, which GHC can find in
- GHC.Magic.Dict.hi.
-
- Because we define a binding for `withDict`, we have to provide a right-hand
- side for its definition. We somewhat arbitrarily choose:
-
- withDict = panicError "Non rewritten withDict"#
-
- This should never be reachable anyway, but just in case ds_withDict fails
- to rewrite away `withDict`, this ensures that the program won't get very far.
-
-(WD7) One could conceivably implement this special case for `withDict` as a
- constant-folding rule instead of during desugaring. We choose not to do so
- for the following reasons:
-
- - Having a constant-folding rule would require that `withDict`'s definition
- be wired in to the compiler so as to prevent `withDict` from inlining too
- early. Implementing the special case in the desugarer, on the other hand,
- only requires that `withDict` be known-key.
-
- - If the constant-folding rule were to fail, we want to throw a compile-time
- error, which is trickier to do with the way that GHC.Core.Opt.ConstantFold
- is set up.
-
-(WD8) In fact we desugar `withDict @{rr} @mtype @(C t_1 ... t_n) @r` to
- let wd = \sv k -> k (sv |> co)
- {-# INLINE [2] #-}
- in wd
-
- The local `let` and INLINE pragma delays inlining `wd` until after the
- type-class Specialiser has run. This is super important. Suppose we
- have calls
- withDict A k
- withDict B k
- where k1, k2 :: C T -> blah. If we inline those withDict calls we'll get
- k (A |> co1)
- k (B |> co2)
- and the Specialiser will assume that those arguments (of type `C T`) are
- the same, will specialise `k` for that type, and will call the same,
- specialised function from both call sites. #21575 is a concrete case in point.
-
- Solution: delay inlining `withDict` until after the specialiser; that is,
- until Phase 2. This is not a Final Solution -- seee #21575 "Alas..".
--}
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 50a13ba901..f2ffeea8c6 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -38,14 +38,19 @@ import GHC.Types.Var
import GHC.Core.Predicate
import GHC.Core.InstEnv
import GHC.Core.Type
-import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS )
+import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS, mkCoreLams )
import GHC.Core.DataCon
import GHC.Core.TyCon
import GHC.Core.Class
+import GHC.Core ( Expr(Var, App, Cast, Let), Bind (NonRec) )
+import GHC.Types.Basic
+import GHC.Types.SourceText
+
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc( splitAtList, fstOf3 )
+import GHC.Data.FastString
import Data.Maybe
@@ -155,6 +160,7 @@ matchGlobalInst dflags short_cut clas tys
= matchKnownChar dflags short_cut clas tys
| isCTupleClass clas = matchCTuple clas tys
| cls_name == typeableClassName = matchTypeable clas tys
+ | cls_name == withDictClassName = matchWithDict tys
| clas `hasKey` heqTyConKey = matchHeteroEquality tys
| clas `hasKey` eqTyConKey = matchHomoEquality tys
| clas `hasKey` coercibleTyConKey = matchCoercible tys
@@ -431,6 +437,178 @@ makeLitDict clas ty et
{- ********************************************************************
* *
+ Class lookup for WithDict
+* *
+***********************************************************************-}
+
+-- See Note [withDict]
+matchWithDict :: [Type] -> TcM ClsInstResult
+matchWithDict [cls, mty]
+ -- Check that cls is a class constraint `C t_1 ... t_n`, where
+ -- `dict_tc = C` and `dict_args = t_1 ... t_n`.
+ | Just (dict_tc, dict_args) <- tcSplitTyConApp_maybe cls
+ -- Check that C is a class of the form
+ -- `class C a_1 ... a_n where op :: meth_ty`
+ -- and in that case let
+ -- co :: C t1 ..tn ~R# inst_meth_ty
+ , Just (inst_meth_ty, co) <- tcInstNewTyCon_maybe dict_tc dict_args
+ = do { sv <- mkSysLocalM (fsLit "withDict_s") Many mty
+ ; k <- mkSysLocalM (fsLit "withDict_k") Many (mkInvisFunTyMany cls openAlphaTy)
+
+ ; let evWithDict_type = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] $
+ mkVisFunTysMany [mty, mkInvisFunTyMany cls openAlphaTy] openAlphaTy
+
+ ; wd_id <- mkSysLocalM (fsLit "withDict_wd") Many evWithDict_type
+ ; let wd_id' = wd_id `setInlinePragma` inlineAfterSpecialiser
+
+ -- Given co2 : mty ~N# inst_meth_ty, construct the method of
+ -- the WithDict dictionary:
+ -- \@(r : RuntimeRep) @(a :: TYPE r) (sv : mty) (k :: cls => a) -> k (sv |> (sub co; sym co2))
+ ; let evWithDict co2 =
+ let wd_rhs = mkCoreLams [ runtimeRep1TyVar, openAlphaTyVar, sv, k ] $
+ Var k `App` Cast (Var sv) (mkTcTransCo (mkTcSubCo co2) (mkTcSymCo co))
+ in Let (NonRec wd_id' wd_rhs) (Var wd_id')
+ -- Why a Let? See (WD6) in Note [withDict]
+
+ ; tc <- tcLookupTyCon withDictClassName
+ ; let Just withdict_data_con
+ = tyConSingleDataCon_maybe tc -- "Data constructor"
+ -- for WithDict
+ mk_ev [c] = evDataConApp withdict_data_con
+ [cls, mty] [evWithDict (evTermCoercion (EvExpr c))]
+ mk_ev e = pprPanic "matchWithDict" (ppr e)
+
+ ; return $ OneInst { cir_new_theta = [mkPrimEqPred mty inst_meth_ty]
+ , cir_mk_ev = mk_ev
+ , cir_what = BuiltinInstance }
+ }
+
+matchWithDict _
+ = return NoInstance
+
+inlineAfterSpecialiser :: InlinePragma
+-- Do not inline before the specialiser; but do so afterwards
+-- See (WD6) in Note [withDict]
+inlineAfterSpecialiser = alwaysInlinePragma `setInlinePragmaActivation`
+ ActiveAfter NoSourceText 2
+
+{-
+Note [withDict]
+~~~~~~~~~~~~~~~
+The class `WithDict` is defined as:
+
+ class WithDict cls meth where
+ withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
+
+This class is special, like `Typeable`: GHC automatically solves
+for instances of `WithDict`, users cannot write their own.
+
+It is used to implement a primitive that we cannot define in Haskell
+but we can write in Core.
+
+`WithDict` is used to create dictionaries for classes with a single method.
+Consider a class like this:
+
+ class C a where
+ f :: T a
+
+We can use `withDict` to cast values of type `T a` into dictionaries for `C a`.
+To do this, we can define a function like this in the library:
+
+ withT :: T a -> (C a => b) -> b
+ withT t k = withDict @(C a) @(T a) t k
+
+Here:
+
+* The `cls` in `withDict` is instantiated to `C a`.
+
+* The `meth` in `withDict` is instantiated to `T a`.
+ The definition of `T` itself is irrelevant, only that `C a` is a class
+ with a single method of type `T a`.
+
+* The `r` in `withDict` is instantiated to `b`.
+
+For any single-method class C:
+ class C a1 .. an where op :: meth_ty
+
+The solver will solve the constraint `WithDict (C t1 .. tn) mty`
+as if the following instance declaration existed:
+
+instance (mty ~# inst_meth_ty) => WithDict (C t1..tn) mty where
+ withDict = \@{rr} @(r :: TYPE rr) (sv :: mty) (k :: C t1..tn => r) ->
+ k (sv |> (sub co2; sym co))
+
+That is, it matches on the first (constraint) argument of C; if C is
+a single-method class, the instance "fires" and emits an equality
+constraint `mty ~ inst_meth_ty`, where `inst_meth_ty` is `meth_ty[ti/ai]`.
+The coercion `co2` witnesses the equality `mty ~ inst_meth_ty`.
+
+The coercion `co` is a newtype coercion that coerces from `C t1 ... tn`
+to `inst_meth_ty`.
+This coercion is guaranteed to exist by virtue of the fact that
+C is a class with exactly one method and no superclasses, so it
+is treated like a newtype when compiled to Core.
+
+The condition that `C` is a single-method class is implemented in the
+guards of matchWithDict's definition.
+If the conditions are not held, the rewriting will not fire,
+and we'll report an unsolved constraint.
+
+Some further observations about `withDict`:
+
+(WD1) The `cls` in the type of withDict must be explicitly instantiated with
+ visible type application, as invoking `withDict` would be ambiguous
+ otherwise.
+
+ For examples of how `withDict` is used in the `base` library, see `withSNat`
+ in GHC.TypeNats, as well as `withSChar` and `withSSymbol` in GHC.TypeLits.
+
+(WD2) The `r` is representation-polymorphic, to support things like
+ `withTypeable` in `Data.Typeable.Internal`.
+
+(WD3) As an alternative to `withDict`, one could define functions like `withT`
+ above in terms of `unsafeCoerce`. This is more error-prone, however.
+
+(WD4) In order to define things like `reifySymbol` below:
+
+ reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
+
+ `withDict` needs to be instantiated with `Any`, like so:
+
+ reifySymbol n k = withDict @(KnownSymbol Any) @String @r n (k @Any)
+
+ The use of `Any` is explained in Note [NOINLINE someNatVal] in
+ base:GHC.TypeNats.
+
+(WD5) In earlier implementations, `withDict` was implemented as an identifier
+ with special handling during either constant-folding or desugaring.
+ The current approach is more robust, previously the type of `withDict`
+ did not have a type-class constraint and was overly polymorphic.
+ See #19915.
+
+(WD6) In fact we desugar `withDict @(C t_1 ... t_n) @mty @{rr} @r` to
+ let wd = \sv k -> k (sv |> co)
+ {-# INLINE [2] #-}
+ in wd
+ The local `let` and INLINE pragma delays inlining `wd` until after the
+ type-class Specialiser has run. This is super important. Suppose we
+ have calls
+ withDict A k
+ withDict B k
+ where k1, k2 :: C T -> blah. If we inline those withDict calls we'll get
+ k (A |> co1)
+ k (B |> co2)
+ and the Specialiser will assume that those arguments (of type `C T`) are
+ the same, will specialise `k` for that type, and will call the same,
+ specialised function from both call sites. #21575 is a concrete case in point.
+
+ Solution: delay inlining `withDict` until after the specialiser; that is,
+ until Phase 2. This is not a Final Solution -- seee #21575 "Alas..".
+
+-}
+
+{- ********************************************************************
+* *
Class lookup for Typeable
* *
***********************************************************************-}
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 9010c43d46..22b627a36f 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1407,7 +1407,7 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
-- 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 `elem` [ heqTyConName, eqTyConName, coercibleTyConName ]
+ | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName, withDictClassName ]
, not quantified_constraint
= failWithTc $ TcRnSpecialClassInst clas False
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index b1441fee84..2d2f735351 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -542,7 +542,7 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
-- @
withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
=> TypeRep a -> (Typeable a => r) -> r
-withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k
+withTypeable rep k = withDict @(Typeable a) rep k
-- | Pattern match on a type constructor
pattern Con :: forall k (a :: k). ()
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index d4a59b440c..d9793d59d7 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -124,7 +124,7 @@ module GHC.Exts
unsafeCoerce#,
-- ** Casting class dictionaries with single methods
- withDict,
+ WithDict(..),
-- * The maximum tuple size
maxTupleSize,
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 97b922c79e..a2310fd998 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -261,16 +261,16 @@ cmpChar x y = case compare (charVal x) (charVal y) of
newtype SSymbol (s :: Symbol) = SSymbol String
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
withSSymbol :: forall a b.
(KnownSymbol a => Proxy a -> b)
-> SSymbol a -> Proxy a -> b
-withSSymbol f x y = withDict @(SSymbol a) @(KnownSymbol a) x f y
+withSSymbol f x y = withDict @(KnownSymbol a) x f y
newtype SChar (s :: Char) = SChar Char
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
withSChar :: forall a b.
(KnownChar a => Proxy a -> b)
-> SChar a -> Proxy a -> b
-withSChar f x y = withDict @(SChar a) @(KnownChar a) x f y
+withSChar f x y = withDict @(KnownChar a) x f y
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index e764ed47db..6a71313404 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -39,7 +39,7 @@ module GHC.TypeNats
) where
-import GHC.Base(Eq(..), Ord(..), otherwise, withDict)
+import GHC.Base(Eq(..), Ord(..), otherwise, WithDict(..))
import GHC.Types
import GHC.Num.Natural(Natural)
import GHC.Show(Show(..))
@@ -125,7 +125,7 @@ After inlining and simplification, this ends up looking something like this:
where type T = Any Nat
`KnownNat` is the constructor for dictionaries for the class `KnownNat`.
-See Note [withDict] in "GHC.HsToCore.Expr" for details on how
+See Note [withDict] in "GHC.Tc.Instance.Class" for details on how
we actually construct the dictionary.
Note that using `Any Nat` is not really correct, as multiple calls to
@@ -245,8 +245,8 @@ cmpNat x y = case compare (natVal x) (natVal y) of
newtype SNat (n :: Nat) = SNat Natural
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
withSNat :: forall a b.
(KnownNat a => Proxy a -> b)
-> SNat a -> Proxy a -> b
-withSNat f x y = withDict @(SNat a) @(KnownNat a) x f y
+withSNat f x y = withDict @(KnownNat a) x f y
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index 12861db568..560ab3956f 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
-{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
@@ -18,7 +18,7 @@
-- Portability : non-portable (GHC Extensions)
--
-- Defines the 'withDict' function. For more information, see
--- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC.
+-- @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
-- The definition of 'withDict' is located in a separate module from
-- "GHC.Magic" because 'withDict' is @Unsafe@ (it threatens type class
-- coherence) while "GHC.Magic" is @Trustworthy@.
@@ -28,9 +28,8 @@
--
-----------------------------------------------------------------------------
-module GHC.Magic.Dict (withDict) where
+module GHC.Magic.Dict (WithDict(..)) where
-import GHC.Prim.Panic (panicError)
import GHC.Types (RuntimeRep, TYPE)
-- | @'withDict' d f@ provides a way to call a type-class–overloaded function
@@ -38,7 +37,6 @@ import GHC.Types (RuntimeRep, TYPE)
--
-- 'withDict' can only be used if the type class has a single method with no
-- superclasses. For more (important) details on how this works, see
--- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC.
-withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
-{-# NOINLINE withDict #-}
-withDict = panicError "Non-rewritten withDict"#
+-- @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
+class WithDict cls meth where
+ withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 45701629a4..049b254743 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -4,7 +4,8 @@
`GHC.Magic.Dict` instead of `GHC.Prim`. `withDict` now has the type:
```
- withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
+ class WithDict cls meth where
+ withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
```
Unlike `magicDict`, `withDict` can be used without defining an
@@ -14,10 +15,10 @@
```
withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
=> TypeRep a -> (Typeable a => r) -> r
- withTypeable rep k = withDict @(TypeRep a) @(Typeable a) rep k
+ withTypeable rep k = withDict @(Typeable a) rep k
```
- Note that the explicit type applications are required, as the call to
+ Note that the explicit type application is required, as the call to
`withDict` would be ambiguous otherwise.
- Primitive types and functions which handle boxed values are now levity-polymorphic,
diff --git a/testsuite/tests/ghci/scripts/T19667Ghci.hs b/testsuite/tests/ghci/scripts/T19667Ghci.hs
index c3ffa71be8..bc8f36de93 100644
--- a/testsuite/tests/ghci/scripts/T19667Ghci.hs
+++ b/testsuite/tests/ghci/scripts/T19667Ghci.hs
@@ -21,7 +21,7 @@ symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
-- See Note [NOINLINE someNatVal] in GHC.TypeNats
{-# NOINLINE reifySymbol #-}
reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
-reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
+reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
main :: IO ()
main = print $ reifySymbol "Hello World" symbolVal
diff --git a/testsuite/tests/simplCore/should_run/T21575.hs b/testsuite/tests/simplCore/should_run/T21575.hs
index 976483f963..d1b383ec1a 100644
--- a/testsuite/tests/simplCore/should_run/T21575.hs
+++ b/testsuite/tests/simplCore/should_run/T21575.hs
@@ -31,7 +31,7 @@ main = do
toJSONBar :: Given Style => Bar -> Value
give Normal (\gd -> toJSONBar gd e)
- --> withDict @Style @(Given Style) Normal (toJSON e)
+ --> withDict @(Given Style) @Style Normal (toJSON e)
--> toJSONBar ((Normal |> co) :: Given Style) e
give Normal (\gd -> toJSONBar gd e')
@@ -40,7 +40,7 @@ toJSONBar :: Given Style => Bar -> Value
--------- With new cast ------------
give Normal (\gd -> toJSONBar gd e)
- --> withDict @Style @(Given Style) Normal (\gd -> toJSONBar gd e)
+ --> withDict @(Given Style) @Style Normal (\gd -> toJSONBar gd e)
--> ((\gd -> toJSONBar gd e) |> co) Normal
--> (\gd' -> toJSonBar (gd' |> sym (co[1])) e) Normal
--> toJSONBar (Normal |> co') e -- Boo!
@@ -61,7 +61,7 @@ class Given a where
give :: forall a r. a -> (Given a => r) -> r
#if WITH_DICT
-give = withDict @a @(Given a)
+give = withDict @(Given a) @a
#else
give a k = unsafeCoerce (Gift k :: Gift a r) a
diff --git a/testsuite/tests/typecheck/should_compile/T21328.hs b/testsuite/tests/typecheck/should_compile/T21328.hs
new file mode 100644
index 0000000000..9b72df193f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21328.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+module T21328 where
+
+import GHC.Exts
+import Type.Reflection
+
+type family F x
+type instance F x = x
+
+type family G x
+type instance G x = x
+
+class C a where
+ m :: G a
+
+cast :: forall a. F a -> (C a => Int) -> Int
+cast = withDict @(C a) @(F a)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f08828eeea..a258f6de03 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -829,6 +829,7 @@ test('T21023', normal, compile, ['-ddump-types'])
test('T21205', normal, compile, ['-O0'])
test('T21323', normal, compile, [''])
test('T21315', normal, compile, ['-Wredundant-constraints'])
+test('T21328', normal, compile, [''])
test('T21516', normal, compile, [''])
test('T21519', normal, compile, [''])
test('T21519a', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.hs b/testsuite/tests/typecheck/should_fail/T16646Fail.hs
index 73ded574b7..bf3cfcc6f3 100644
--- a/testsuite/tests/typecheck/should_fail/T16646Fail.hs
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail.hs
@@ -12,17 +12,11 @@ import Data.Kind
import Data.Proxy
import GHC.Exts
-f :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
-f = withDict @st @dt
+f :: forall {rr :: RuntimeRep} cls meth (r :: TYPE rr). meth -> (cls => r) -> r
+f = withDict @cls @meth
class Show a => C a where
m :: Maybe a
g :: forall a r. Maybe a -> (C a => r) -> r
-g = withDict @(Maybe a) @(C a)
-
-class Reifies s a | s -> a where
- reflect :: proxy s -> a
-
-reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
-reify a k = withDict @_ @(Reifies (Any @Type) a) (const a) (k @Any) Proxy
+g = withDict @(C a) @(Maybe a)
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.stderr b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
index 3873a096d9..4c597bed33 100644
--- a/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
@@ -1,11 +1,15 @@
T16646Fail.hs:16:5: error:
- Invalid instantiation of ‘withDict’ at type: st -> (dt => r) -> r
+ • No instance for (WithDict cls meth) arising from a use of ‘withDict’
+ Possible fix:
+ add (WithDict cls meth) to the context of
+ the type signature for:
+ f :: forall (cls :: Constraint) meth r. meth -> (cls => r) -> r
+ • In the expression: withDict @cls @meth
+ In an equation for ‘f’: f = withDict @cls @meth
T16646Fail.hs:22:5: error:
- Invalid instantiation of ‘withDict’ at type:
- Maybe a -> (C a => r) -> r
-
-T16646Fail.hs:28:13: error:
- Invalid instantiation of ‘withDict’ at type:
- (Any -> a) -> (Reifies Any a => Proxy Any -> r) -> Proxy Any -> r
+ • No instance for (WithDict (C a) (Maybe a))
+ arising from a use of ‘withDict’
+ • In the expression: withDict @(C a) @(Maybe a)
+ In an equation for ‘g’: g = withDict @(C a) @(Maybe a)
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail2.hs b/testsuite/tests/typecheck/should_fail/T16646Fail2.hs
new file mode 100644
index 0000000000..55934f7474
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail2.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T16646Fail where
+
+import Data.Kind
+import Data.Proxy
+import GHC.Exts
+
+class Reifies s a | s -> a where
+ reflect :: proxy s -> a
+
+reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
+reify a k = withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr b/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr
new file mode 100644
index 0000000000..7a8178136c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr
@@ -0,0 +1,16 @@
+
+T16646Fail2.hs:19:13: error:
+ • Couldn't match type: b0 -> a
+ with: forall (proxy :: * -> *). proxy Any -> a
+ arising from a use of ‘withDict’
+ • In the expression:
+ withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
+ In an equation for ‘reify’:
+ reify a k
+ = withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
+ • Relevant bindings include
+ k :: forall s. Reifies s a => Proxy s -> r
+ (bound at T16646Fail2.hs:19:9)
+ a :: a (bound at T16646Fail2.hs:19:7)
+ reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r
+ (bound at T16646Fail2.hs:19:1)
diff --git a/testsuite/tests/typecheck/should_fail/T19915.hs b/testsuite/tests/typecheck/should_fail/T19915.hs
new file mode 100644
index 0000000000..9f7ac26389
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19915.hs
@@ -0,0 +1,5 @@
+module T19915 where
+
+import GHC.Exts
+
+instance WithDict a b
diff --git a/testsuite/tests/typecheck/should_fail/T19915.stderr b/testsuite/tests/typecheck/should_fail/T19915.stderr
new file mode 100644
index 0000000000..7f75999605
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19915.stderr
@@ -0,0 +1,4 @@
+
+T19915.hs:5:10: error:
+ • Class ‘WithDict’ does not support user-specified instances.
+ • In the instance declaration for ‘WithDict a b’
diff --git a/testsuite/tests/typecheck/should_fail/T21328.hs b/testsuite/tests/typecheck/should_fail/T21328.hs
deleted file mode 100644
index f589c5d3a7..0000000000
--- a/testsuite/tests/typecheck/should_fail/T21328.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-module T21328 where
-
-import GHC.Exts
-import Type.Reflection
-
-type family Id x
-type instance Id x = x
-
-cast :: forall a. Id (TypeRep a) -> (Typeable a => Int) -> Int
-cast = withDict @(TypeRep a) @(Typeable a)
diff --git a/testsuite/tests/typecheck/should_fail/T21328.stderr b/testsuite/tests/typecheck/should_fail/T21328.stderr
deleted file mode 100644
index a7d106a793..0000000000
--- a/testsuite/tests/typecheck/should_fail/T21328.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T21328.hs:11:8: error:
- Invalid instantiation of ‘withDict’ at type:
- Id (TypeRep a) -> (Typeable a => Int) -> Int
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 83ba2c4414..46fecd51ce 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -530,6 +530,7 @@ test('T16627', normal, compile_fail, [''])
test('T502', normal, compile_fail, [''])
test('T16517', normal, compile_fail, [''])
test('T16646Fail', normal, compile_fail, [''])
+test('T16646Fail2', normal, compile_fail, [''])
test('T15883', normal, compile_fail, [''])
test('T15883b', normal, compile_fail, [''])
test('T15883c', normal, compile_fail, [''])
@@ -629,6 +630,7 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
['T19397E4.hs', '-v0 -main-is foo'])
test('T19415', normal, compile_fail, [''])
+test('T19915', normal, compile_fail, [''])
test('T19977a', normal, compile_fail, [''])
test('T19977b', normal, compile_fail, [''])
test('T19978', normal, compile_fail, [''])
@@ -653,6 +655,5 @@ test('T20064', normal, compile_fail, [''])
test('T21130', normal, compile_fail, [''])
test('T20768_fail', normal, compile_fail, [''])
test('T21327', normal, compile_fail, [''])
-test('T21328', normal, compile_fail, [''])
test('T21338', normal, compile_fail, [''])
test('T21158', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs
index 6af86e96a4..0976215ae9 100644
--- a/testsuite/tests/typecheck/should_run/T16646.hs
+++ b/testsuite/tests/typecheck/should_run/T16646.hs
@@ -22,8 +22,8 @@ instance KnownNat n => Reifies n Integer where
reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
{-# NOINLINE reify #-} -- See Note [NOINLINE someNatVal] in GHC.TypeNats
-reify a k = withDict @(forall (proxy :: Type -> Type). proxy Any -> a)
- @(Reifies (Any @Type) a)
+reify a k = withDict @(Reifies (Any @Type) a)
+ @(forall (proxy :: Type -> Type). proxy Any -> a)
(const a) (k @Any) Proxy
class Given a where
@@ -32,7 +32,7 @@ class Given a where
withGift :: forall a b.
(Given a => Proxy a -> b)
-> a -> Proxy a -> b
-withGift f x y = withDict @a @(Given a) x f y
+withGift f x y = withDict @(Given a) @a x f y
give :: forall a r. a -> (Given a => r) -> r
give a k = withGift (\_ -> k) a Proxy
@@ -62,7 +62,7 @@ singInstance :: forall k (a :: k). Sing a -> SingInstance a
singInstance s = with_sing_i SingInstance
where
with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
- with_sing_i si = withDict @(Sing a) @(SingI a) s si
+ with_sing_i si = withDict @(SingI a) @(Sing a) s si
withSingI :: Sing n -> (SingI n => r) -> r
withSingI sn r =
diff --git a/testsuite/tests/typecheck/should_run/T19667.hs b/testsuite/tests/typecheck/should_run/T19667.hs
index c3ffa71be8..bc8f36de93 100644
--- a/testsuite/tests/typecheck/should_run/T19667.hs
+++ b/testsuite/tests/typecheck/should_run/T19667.hs
@@ -21,7 +21,7 @@ symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
-- See Note [NOINLINE someNatVal] in GHC.TypeNats
{-# NOINLINE reifySymbol #-}
reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
-reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
+reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
main :: IO ()
main = print $ reifySymbol "Hello World" symbolVal