Refactor validity checking for constraints
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 4 Jul 2018 14:17:54 +0000 (15:17 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 5 Jul 2018 09:44:23 +0000 (10:44 +0100)
There are several changes here.

* TcInteract has gotten too big, so I moved all the class-instance
  matching out of TcInteract into a new module ClsInst. It parallels
  the FamInst module.

  The main export of ClsInst is matchGlobalInst.
  This now works in TcM not TcS.

* A big reason to make matchGlobalInst work in TcM is that we can
  then use it from TcValidity.checkSimplifiableClassConstraint.
  That extends checkSimplifiableClassConstraint to work uniformly
  for built-in instances, which means that we now get a warning
  if we have givens (Typeable x, KnownNat n); see Trac #15322.

* This change also made me refactor LookupInstResult, in particular
  by adding the InstanceWhat field.  I also changed the name of the
  type to ClsInstResult.

  Then instead of matchGlobalInst reporting a staging error (which is
  inappropriate for the call from TcValidity), we can do so in
  TcInteract.checkInstanceOK.

* In TcValidity, we now check quantified constraints for termination.
  For example, this signature should be rejected:
     f :: (forall a. Eq (m a) => Eq (m a)) => blah
  as discussed in Trac #15316.   The main change here is that
  TcValidity.check_pred_help now uses classifyPredType, and has a
  case for ForAllPred which it didn't before.

  This had knock-on refactoring effects in TcValidity.

23 files changed:
compiler/ghc.cabal.in
compiler/typecheck/ClsInst.hs [new file with mode: 0644]
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/indexed-types/should_compile/T15322.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T15322.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T15322a.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T15322a.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/partial-sigs/should_compile/SomethingShowable.stderr
testsuite/tests/polykinds/T11466.stderr
testsuite/tests/quantified-constraints/T15316.hs [new file with mode: 0644]
testsuite/tests/quantified-constraints/T15316.stderr [new file with mode: 0644]
testsuite/tests/quantified-constraints/all.T
testsuite/tests/typecheck/should_compile/T10177.hs
testsuite/tests/typecheck/should_compile/T13526.stderr
testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs
testsuite/tests/typecheck/should_fail/T8912.stderr
testsuite/tests/typecheck/should_fail/fd-loop.stderr
testsuite/tests/typecheck/should_fail/tcfail157.stderr
testsuite/tests/typecheck/should_fail/tcfail211.stderr

index 01628dc..d4a1dc3 100644 (file)
@@ -437,6 +437,7 @@ Library
         WorkWrap
         WwLib
         FamInst
+        ClsInst
         Inst
         TcAnnotations
         TcArrows
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
new file mode 100644 (file)
index 0000000..b8ab2bf
--- /dev/null
@@ -0,0 +1,586 @@
+{-# LANGUAGE CPP #-}
+
+module ClsInst (
+     matchGlobalInst,
+     ClsInstResult(..),
+     InstanceWhat(..), safeOverlap
+  ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import TcEnv
+import TcRnMonad
+import TcType
+import TcMType
+import TcEvidence
+import RnEnv( addUsedGRE )
+import RdrName( lookupGRE_FieldLabel )
+import InstEnv
+import Inst( instDFunType )
+import FamInst( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
+
+import TysWiredIn
+import TysPrim( eqPrimTyCon, eqReprPrimTyCon )
+import PrelNames
+
+import Id
+import Type
+import Kind( isConstraintKind )
+import MkCore ( mkStringExprFS, mkNaturalExpr )
+
+import Unique ( hasKey )
+import Name   ( Name )
+import Var    ( DFunId )
+import DataCon
+import TyCon
+import Class
+import DynFlags
+import Outputable
+import Util( splitAtList, fstOf3 )
+import Data.Maybe
+
+{- *******************************************************************
+*                                                                    *
+                       Class lookup
+*                                                                    *
+**********************************************************************-}
+
+-- | Indicates if Instance met the Safe Haskell overlapping instances safety
+-- check.
+--
+-- See Note [Safe Haskell Overlapping Instances] in TcSimplify
+-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
+type SafeOverlapping = Bool
+
+data ClsInstResult
+  = NoInstance   -- Definitely no instance
+
+  | OneInst { cir_new_theta :: [TcPredType]
+            , cir_mk_ev     :: [EvExpr] -> EvTerm
+            , cir_what      :: InstanceWhat }
+
+  | NotSure      -- Multiple matches and/or one or more unifiers
+
+data InstanceWhat
+  = BuiltinInstance
+  | LocalInstance
+  | TopLevInstance { iw_dfun_id   :: DFunId
+                   , iw_safe_over :: SafeOverlapping }
+
+instance Outputable ClsInstResult where
+  ppr NoInstance = text "NoInstance"
+  ppr NotSure    = text "NotSure"
+  ppr (OneInst { cir_new_theta = ev
+               , cir_what = what })
+    = text "OneInst" <+> vcat [ppr ev, ppr what]
+
+instance Outputable InstanceWhat where
+  ppr BuiltinInstance = text "built-in instance"
+  ppr LocalInstance   = text "locally-quantified instance"
+  ppr (TopLevInstance { iw_safe_over = so })
+     = text "top-level instance" <+> (text $ if so then "[safe]" else "[unsafe]")
+
+safeOverlap :: InstanceWhat -> Bool
+safeOverlap (TopLevInstance { iw_safe_over = so }) = so
+safeOverlap _                                      = True
+
+matchGlobalInst :: DynFlags
+                -> Bool      -- True <=> caller is the short-cut solver
+                             -- See Note [Shortcut solving: overlap]
+                -> Class -> [Type] -> TcM ClsInstResult
+matchGlobalInst dflags short_cut clas tys
+  | cls_name == knownNatClassName     = matchKnownNat        clas tys
+  | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
+  | isCTupleClass clas                = matchCTuple          clas tys
+  | cls_name == typeableClassName     = matchTypeable        clas tys
+  | clas `hasKey` heqTyConKey         = matchLiftedEquality       tys
+  | clas `hasKey` coercibleTyConKey   = matchLiftedCoercible      tys
+  | cls_name == hasFieldClassName     = matchHasField dflags short_cut clas tys
+  | otherwise                         = matchInstEnv dflags short_cut clas tys
+  where
+    cls_name = className clas
+
+
+{- ********************************************************************
+*                                                                     *
+                   Looking in the instance environment
+*                                                                     *
+***********************************************************************-}
+
+
+matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
+matchInstEnv dflags short_cut_solver clas tys
+   = do { instEnvs <- tcGetInstEnvs
+        ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
+              (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
+              safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
+        ; traceTc "matchInstEnv" $
+            vcat [ text "goal:" <+> ppr clas <+> ppr tys
+                 , text "matches:" <+> ppr matches
+                 , text "unify:" <+> ppr unify ]
+        ; case (matches, unify, safeHaskFail) of
+
+            -- Nothing matches
+            ([], [], _)
+                -> do { traceTc "matchClass not matching" (ppr pred)
+                      ; return NoInstance }
+
+            -- A single match (& no safe haskell failure)
+            ([(ispec, inst_tys)], [], False)
+                | short_cut_solver      -- Called from the short-cut solver
+                , isOverlappable ispec
+                -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
+                -- then don't let the short-cut solver choose it, because a
+                -- later instance might overlap it.  Trac #14434 is an example
+                -- See Note [Shortcut solving: overlap]
+                -> do { traceTc "matchClass: ignoring overlappable" (ppr pred)
+                      ; return NotSure }
+
+                | otherwise
+                -> do { let dfun_id = instanceDFunId ispec
+                      ; traceTc "matchClass success" $
+                        vcat [text "dict" <+> ppr pred,
+                              text "witness" <+> ppr dfun_id
+                                             <+> ppr (idType dfun_id) ]
+                                -- Record that this dfun is needed
+                      ; match_one (null unsafeOverlaps) dfun_id inst_tys }
+
+            -- More than one matches (or Safe Haskell fail!). Defer any
+            -- reactions of a multitude until we learn more about the reagent
+            _   -> do { traceTc "matchClass multiple matches, deferring choice" $
+                        vcat [text "dict" <+> ppr pred,
+                              text "matches" <+> ppr matches]
+                      ; return NotSure } }
+   where
+     pred = mkClassPred clas tys
+
+match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult
+             -- See Note [DFunInstType: instantiating types] in InstEnv
+match_one so dfun_id mb_inst_tys
+  = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
+       ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
+       ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
+       ; return $ OneInst { cir_new_theta = theta
+                          , cir_mk_ev     = evDFunApp dfun_id tys
+                          , cir_what      = TopLevInstance { iw_dfun_id = dfun_id
+                                                           , iw_safe_over = so } } }
+
+
+{- ********************************************************************
+*                                                                     *
+                   Class lookup for CTuples
+*                                                                     *
+***********************************************************************-}
+
+matchCTuple :: Class -> [Type] -> TcM ClsInstResult
+matchCTuple clas tys   -- (isCTupleClass clas) holds
+  = return (OneInst { cir_new_theta = tys
+                    , cir_mk_ev     = tuple_ev
+                    , cir_what      = BuiltinInstance })
+            -- The dfun *is* the data constructor!
+  where
+     data_con = tyConSingleDataCon (classTyCon clas)
+     tuple_ev = evDFunApp (dataConWrapId data_con) tys
+
+{- ********************************************************************
+*                                                                     *
+                   Class lookup for Literals
+*                                                                     *
+***********************************************************************-}
+
+{-
+Note [KnownNat & KnownSymbol and EvLit]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A part of the type-level literals implementation are the classes
+"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
+defining singleton values.  Here is the key stuff from GHC.TypeLits
+
+  class KnownNat (n :: Nat) where
+    natSing :: SNat n
+
+  newtype SNat (n :: Nat) = SNat Integer
+
+Conceptually, this class has infinitely many instances:
+
+  instance KnownNat 0       where natSing = SNat 0
+  instance KnownNat 1       where natSing = SNat 1
+  instance KnownNat 2       where natSing = SNat 2
+  ...
+
+In practice, we solve `KnownNat` predicates in the type-checker
+(see typecheck/TcInteract.hs) because we can't have infinitely many instances.
+The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
+
+We make the following assumptions about dictionaries in GHC:
+  1. The "dictionary" for classes with a single method---like `KnownNat`---is
+     a newtype for the type of the method, so using a evidence amounts
+     to a coercion, and
+  2. Newtypes use the same representation as their definition types.
+
+So, the evidence for `KnownNat` is just a value of the representation type,
+wrapped in two newtype constructors: one to make it into a `SNat` value,
+and another to make it into a `KnownNat` dictionary.
+
+Also note that `natSing` and `SNat` are never actually exposed from the
+library---they are just an implementation detail.  Instead, users see
+a more convenient function, defined in terms of `natSing`:
+
+  natVal :: KnownNat n => proxy n -> Integer
+
+The reason we don't use this directly in the class is that it is simpler
+and more efficient to pass around an integer rather than an entire function,
+especially when the `KnowNat` evidence is packaged up in an existential.
+
+The story for kind `Symbol` is analogous:
+  * class KnownSymbol
+  * newtype SSymbol
+  * Evidence: a Core literal (e.g. mkNaturalExpr)
+-}
+
+matchKnownNat :: Class -> [Type] -> TcM ClsInstResult
+matchKnownNat clas [ty]     -- clas = KnownNat
+  | Just n <- isNumLitTy ty = do
+        et <- mkNaturalExpr n
+        makeLitDict clas ty et
+matchKnownNat _ _           = return NoInstance
+
+matchKnownSymbol :: Class -> [Type] -> TcM ClsInstResult
+matchKnownSymbol clas [ty]  -- clas = KnownSymbol
+  | Just s <- isStrLitTy ty = do
+        et <- mkStringExprFS s
+        makeLitDict clas ty et
+matchKnownSymbol _ _       = return NoInstance
+
+makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult
+-- makeLitDict adds a coercion that will convert the literal into a dictionary
+-- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
+-- in TcEvidence.  The coercion happens in 2 steps:
+--
+--     Integer -> SNat n     -- representation of literal to singleton
+--     SNat n  -> KnownNat n -- singleton to dictionary
+--
+--     The process is mirrored for Symbols:
+--     String    -> SSymbol n
+--     SSymbol n -> KnownSymbol n
+makeLitDict clas ty et
+    | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
+          -- co_dict :: KnownNat n ~ SNat n
+    , [ meth ]   <- classMethods clas
+    , Just tcRep <- tyConAppTyCon_maybe -- SNat
+                      $ funResultTy         -- SNat n
+                      $ dropForAlls         -- KnownNat n => SNat n
+                      $ idType meth         -- forall n. KnownNat n => SNat n
+    , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
+          -- SNat n ~ Integer
+    , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
+    = return $ OneInst { cir_new_theta = []
+                       , cir_mk_ev     = \_ -> ev_tm
+                       , cir_what      = BuiltinInstance }
+
+    | otherwise
+    = pprPanic "makeLitDict" $
+      text "Unexpected evidence for" <+> ppr (className clas)
+      $$ vcat (map (ppr . idType) (classMethods clas))
+
+{- ********************************************************************
+*                                                                     *
+                   Class lookup for Typeable
+*                                                                     *
+***********************************************************************-}
+
+-- | Assumes that we've checked that this is the 'Typeable' class,
+-- and it was applied to the correct argument.
+matchTypeable :: Class -> [Type] -> TcM ClsInstResult
+matchTypeable clas [k,t]  -- clas = Typeable
+  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
+  | isForAllTy k                      = return NoInstance   -- Polytype
+  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
+
+  -- Now cases that do work
+  | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
+  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
+  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
+  | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
+  | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
+  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
+  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
+
+matchTypeable _ _ = return NoInstance
+
+-- | Representation for a type @ty@ of the form @arg -> ret@.
+doFunTy :: Class -> Type -> Type -> Type -> TcM ClsInstResult
+doFunTy clas ty arg_ty ret_ty
+  = return $ OneInst { cir_new_theta = preds
+                     , cir_mk_ev     = mk_ev
+                     , cir_what      = BuiltinInstance }
+  where
+    preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
+    mk_ev [arg_ev, ret_ev] = evTypeable ty $
+                             EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
+    mk_ev _ = panic "TcInteract.doFunTy"
+
+
+-- | Representation for type constructor applied to some kinds.
+-- 'onlyNamedBndrsApplied' has ensured that this application results in a type
+-- of monomorphic kind (e.g. all kind variables have been instantiated).
+doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
+doTyConApp clas ty tc kind_args
+  | Just _ <- tyConRepName_maybe tc
+  = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
+                     , cir_mk_ev     = mk_ev
+                     , cir_what      = BuiltinInstance }
+  | otherwise
+  = return NoInstance
+  where
+    mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
+
+-- | Representation for TyCon applications of a concrete kind. We just use the
+-- kind itself, but first we must make sure that we've instantiated all kind-
+-- polymorphism, but no more.
+onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
+onlyNamedBndrsApplied tc ks
+ = all isNamedTyConBinder used_bndrs &&
+   not (any isNamedTyConBinder leftover_bndrs)
+ where
+   bndrs                        = tyConBinders tc
+   (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
+
+doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
+-- Representation for an application of a type to a type-or-kind.
+--  This may happen when the type expression starts with a type variable.
+--  Example (ignoring kind parameter):
+--    Typeable (f Int Char)                      -->
+--    (Typeable (f Int), Typeable Char)          -->
+--    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
+--    Typeable f
+doTyApp clas ty f tk
+  | isForAllTy (typeKind f)
+  = return NoInstance -- We can't solve until we know the ctr.
+  | otherwise
+  = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
+                     , cir_mk_ev     = mk_ev
+                     , cir_what      = BuiltinInstance }
+  where
+    mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
+    mk_ev _ = panic "doTyApp"
+
+
+-- Emit a `Typeable` constraint for the given type.
+mk_typeable_pred :: Class -> Type -> PredType
+mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
+
+  -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
+  -- we generate a sub-goal for the appropriate class.
+  -- See Note [Typeable for Nat and Symbol]
+doTyLit :: Name -> Type -> TcM ClsInstResult
+doTyLit kc t = do { kc_clas <- tcLookupClass kc
+                  ; let kc_pred    = mkClassPred kc_clas [ t ]
+                        mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
+                        mk_ev _    = panic "doTyLit"
+                  ; return (OneInst { cir_new_theta = [kc_pred]
+                                    , cir_mk_ev     = mk_ev
+                                    , cir_what      = BuiltinInstance }) }
+
+{- Note [Typeable (T a b c)]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For type applications we always decompose using binary application,
+via doTyApp, until we get to a *kind* instantiation.  Example
+   Proxy :: forall k. k -> *
+
+To solve Typeable (Proxy (* -> *) Maybe) we
+  - First decompose with doTyApp,
+    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
+  - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
+
+If we attempt to short-cut by solving it all at once, via
+doTyConApp
+
+(this note is sadly truncated FIXME)
+
+
+Note [No Typeable for polytypes or qualified types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do not support impredicative typeable, such as
+   Typeable (forall a. a->a)
+   Typeable (Eq a => a -> a)
+   Typeable (() => Int)
+   Typeable (((),()) => Int)
+
+See Trac #9858.  For forall's the case is clear: we simply don't have
+a TypeRep for them.  For qualified but not polymorphic types, like
+(Eq a => a -> a), things are murkier.  But:
+
+ * We don't need a TypeRep for these things.  TypeReps are for
+   monotypes only.
+
+ * Perhaps we could treat `=>` as another type constructor for `Typeable`
+   purposes, and thus support things like `Eq Int => Int`, however,
+   at the current state of affairs this would be an odd exception as
+   no other class works with impredicative types.
+   For now we leave it off, until we have a better story for impredicativity.
+
+
+Note [Typeable for Nat and Symbol]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have special Typeable instances for Nat and Symbol.  Roughly we
+have this instance, implemented here by doTyLit:
+      instance KnownNat n => Typeable (n :: Nat) where
+         typeRep = tyepNatTypeRep @n
+where
+   Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a
+
+Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
+runtime value 'n'; it turns it into a string with 'show' and uses
+that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
+See #10348.
+
+Because of this rule it's inadvisable (see #15322) to have a constraint
+    f :: (Typeable (n :: Nat)) => blah
+in a function signature; it gives rise to overlap problems just as
+if you'd written
+    f :: Eq [a] => blah
+-}
+
+{- ********************************************************************
+*                                                                     *
+                   Class lookup for lifted equality
+*                                                                     *
+***********************************************************************-}
+
+-- See also Note [The equality types story] in TysPrim
+matchLiftedEquality :: [Type] -> TcM ClsInstResult
+matchLiftedEquality args
+  = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
+                    , cir_mk_ev     = evDFunApp (dataConWrapId heqDataCon) args
+                    , cir_what      = BuiltinInstance })
+
+-- See also Note [The equality types story] in TysPrim
+matchLiftedCoercible :: [Type] -> TcM ClsInstResult
+matchLiftedCoercible args@[k, t1, t2]
+  = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
+                    , cir_mk_ev     = evDFunApp (dataConWrapId coercibleDataCon)
+                                                args
+                    , cir_what      = BuiltinInstance })
+  where
+    args' = [k, k, t1, t2]
+matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
+
+
+{- ********************************************************************
+*                                                                     *
+              Class lookup for overloaded record fields
+*                                                                     *
+***********************************************************************-}
+
+{-
+Note [HasField instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+
+    data T y = MkT { foo :: [y] }
+
+and `foo` is in scope.  Then GHC will automatically solve a constraint like
+
+    HasField "foo" (T Int) b
+
+by emitting a new wanted
+
+    T alpha -> [alpha] ~# T Int -> b
+
+and building a HasField dictionary out of the selector function `foo`,
+appropriately cast.
+
+The HasField class is defined (in GHC.Records) thus:
+
+    class HasField (x :: k) r a | x r -> a where
+      getField :: r -> a
+
+Since this is a one-method class, it is represented as a newtype.
+Hence we can solve `HasField "foo" (T Int) b` by taking an expression
+of type `T Int -> b` and casting it using the newtype coercion.
+Note that
+
+    foo :: forall y . T y -> [y]
+
+so the expression we construct is
+
+    foo @alpha |> co
+
+where
+
+    co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
+
+is built from
+
+    co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
+
+which is the new wanted, and
+
+    co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
+
+which can be derived from the newtype coercion.
+
+If `foo` is not in scope, or has a higher-rank or existentially
+quantified type, then the constraint is not solved automatically, but
+may be solved by a user-supplied HasField instance.  Similarly, if we
+encounter a HasField constraint where the field is not a literal
+string, or does not belong to the type, then we fall back on the
+normal constraint solver behaviour.
+-}
+
+-- See Note [HasField instances]
+matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
+matchHasField dflags short_cut clas tys
+  = do { fam_inst_envs <- tcGetFamInstEnvs
+       ; rdr_env       <- getGlobalRdrEnv
+       ; case tys of
+           -- We are matching HasField {k} x r a...
+           [_k_ty, x_ty, r_ty, a_ty]
+               -- x should be a literal string
+             | Just x <- isStrLitTy x_ty
+               -- r should be an applied type constructor
+             , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
+               -- use representation tycon (if data family); it has the fields
+             , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
+               -- x should be a field of r
+             , Just fl <- lookupTyConFieldLabel x r_tc
+               -- the field selector should be in scope
+             , Just gre <- lookupGRE_FieldLabel rdr_env fl
+
+             -> do { sel_id <- tcLookupId (flSelector fl)
+                   ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
+
+                         -- The first new wanted constraint equates the actual
+                         -- type of the selector with the type (r -> a) within
+                         -- the HasField x r a dictionary.  The preds will
+                         -- typically be empty, but if the datatype has a
+                         -- "stupid theta" then we have to include it here.
+                   ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
+
+                         -- Use the equality proof to cast the selector Id to
+                         -- type (r -> a), then use the newtype coercion to cast
+                         -- it to a HasField dictionary.
+                         mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
+                           where
+                             co = mkTcSubCo (evTermCoercion (EvExpr ev1))
+                                      `mkTcTransCo` mkTcSymCo co2
+                         mk_ev [] = panic "matchHasField.mk_ev"
+
+                         Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
+                                                              tys
+
+                         tvs = mkTyVarTys (map snd tv_prs)
+
+                     -- The selector must not be "naughty" (i.e. the field
+                     -- cannot have an existentially quantified type), and
+                     -- it must not be higher-rank.
+                   ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
+                     then do { addUsedGRE True gre
+                             ; return OneInst { cir_new_theta = theta
+                                              , cir_mk_ev     = mk_ev
+                                              , cir_what      = BuiltinInstance } }
+                     else matchInstEnv dflags short_cut clas tys }
+
+           _ -> matchInstEnv dflags short_cut clas tys }
index 5d3a988..18d9525 100644 (file)
@@ -8,7 +8,6 @@ module TcInteract (
 #include "HsVersions.h"
 
 import GhcPrelude
-
 import BasicTypes ( SwapFlag(..), isSwapped,
                     infinity, IntWithInf, intGtLimit )
 import TcCanonical
@@ -16,38 +15,23 @@ import TcFlatten
 import TcUnify( canSolveByUnification )
 import VarSet
 import Type
-import Kind( isConstraintKind )
-import InstEnv( DFunInstType, lookupInstEnv
-              , instanceDFunId, isOverlappable )
+import InstEnv( DFunInstType )
 import CoAxiom( sfInteractTop, sfInteractInert )
 
-import TcMType (newMetaTyVars)
-
 import Var
 import TcType
-import Name
-import RdrName ( lookupGRE_FieldLabel )
-import PrelNames ( knownNatClassName, knownSymbolClassName,
-                   typeableClassName,
-                   coercibleTyConKey,
-                   hasFieldClassName,
+import PrelNames ( coercibleTyConKey,
                    heqTyConKey, eqTyConKey, ipClassKey )
-import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
-                    coercibleDataCon, constraintKindTyCon )
-import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
-import Id( idType, isNaughtyRecordSelector )
 import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
 import TyCon
-import DataCon( dataConWrapId )
-import FieldLabel
 import FunDeps
 import FamInst
+import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap )
 import FamInstEnv
 import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
 
 import TcEvidence
-import MkCore ( mkStringExprFS, mkNaturalExpr )
 import Outputable
 
 import TcRnTypes
@@ -1127,21 +1111,20 @@ shortCutSolver dflags ev_w ev_i
       | let pred = ctEvPred ev
             loc  = ctEvLoc  ev
       , ClassPred cls tys <- classifyPredType pred
-      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc
+      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
            ; case inst_res of
-               OneInst { lir_new_theta = preds
-                       , lir_mk_ev = mk_ev
-                       , lir_safe_over = safeOverlap }
-                 | safeOverlap
+               OneInst { cir_new_theta = preds
+                       , cir_mk_ev     = mk_ev
+                       , cir_what      = what }
+                 | safeOverlap what
                  , all isTyFamFree preds  -- Note [Shortcut solving: type families]
                  -> do { let solved_dicts' = addDict solved_dicts cls tys ev
-                             loc'          = bumpCtLocDepth loc
                              -- solved_dicts': it is important that we add our goal
                              -- to the cache before we solve! Otherwise we may end
                              -- up in a loop while solving recursive dictionaries.
 
                        ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
-                       ; lift $ checkReductionDepth loc pred
+                       ; loc' <- lift $ checkInstanceOK loc what pred
 
                        ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
                                   -- Emit work for subgoals but use our local cache
@@ -2232,8 +2215,9 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
    = do { dflags <- getDynFlags
         ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
         ; case lkup_res of
-               OneInst { lir_safe_over = s }
-                  -> do { unless s $ insertSafeOverlapFailureTcS work_item
+               OneInst { cir_what = what }
+                  -> do { unless (safeOverlap what) $
+                          insertSafeOverlapFailureTcS work_item
                         ; when (isWanted ev) $ addSolvedDict ev cls xis
                         ; chooseInstance work_item lkup_res }
                _  ->  -- NoInstance or NotSure
@@ -2264,53 +2248,66 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
 
-chooseInstance :: Ct -> LookupInstResult -> TcS (StopOrContinue Ct)
+chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
 chooseInstance work_item
-               (OneInst { lir_new_theta = theta
-                        , lir_mk_ev     = mk_ev })
+               (OneInst { cir_new_theta = theta
+                        , cir_what      = what
+                        , cir_mk_ev     = mk_ev })
   = do { traceTcS "doTopReact/found instance for" $ ppr ev
-       ; checkReductionDepth deeper_loc pred
-       ; if isDerived ev then finish_derived theta
-                         else finish_wanted  theta mk_ev }
+       ; deeper_loc <- checkInstanceOK loc what pred
+       ; if isDerived ev then finish_derived deeper_loc theta
+                         else finish_wanted  deeper_loc theta mk_ev }
   where
      ev         = ctEvidence work_item
      pred       = ctEvPred ev
      loc        = ctEvLoc ev
-     origin     = ctLocOrigin loc
-     deeper_loc = zap_origin (bumpCtLocDepth loc)
-
-     zap_origin loc  -- After applying an instance we can set ScOrigin to
-                     -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- origin
-       = setCtLocOrigin loc (ScOrigin infinity)
-       | otherwise
-       = loc
 
-     finish_wanted :: [TcPredType]
+     finish_wanted :: CtLoc -> [TcPredType]
                    -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
-     finish_wanted theta mk_ev
+     finish_wanted loc theta mk_ev
         = do { evb <- getTcEvBindsVar
              ; if isNoEvBindsVar evb
                then -- See Note [Instances in no-evidence implications]
                     continueWith work_item
                else
-          do { evc_vars <- mapM (newWanted deeper_loc) theta
+          do { evc_vars <- mapM (newWanted loc) theta
              ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
              ; stopWith ev "Dict/Top (solved wanted)" } }
 
-     finish_derived theta  -- Use type-class instances for Deriveds, in the hope
-       =                   -- of generating some improvements
-                           -- C.f. Example 3 of Note [The improvement story]
-                           -- It's easy because no evidence is involved
-         do { emitNewDeriveds deeper_loc theta
-            ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
+     finish_derived loc theta
+       = -- Use type-class instances for Deriveds, in the hope
+         -- of generating some improvements
+         -- C.f. Example 3 of Note [The improvement story]
+         -- It's easy because no evidence is involved
+         do { emitNewDeriveds loc theta
+            ; traceTcS "finish_derived" (ppr (ctl_depth loc))
             ; stopWith ev "Dict/Top (solved derived)" }
 
 chooseInstance work_item lookup_res
   = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
 
+checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
+-- Check that it's OK to use this insstance:
+--    (a) the use is well staged in the Template Haskell sense
+--    (b) we have not recursed too deep
+-- Returns the CtLoc to used for sub-goals
+checkInstanceOK loc what pred
+  = do { checkWellStagedDFun loc what pred
+       ; checkReductionDepth deeper_loc pred
+       ; return deeper_loc }
+  where
+     deeper_loc = zap_origin (bumpCtLocDepth loc)
+     origin     = ctLocOrigin loc
+
+     zap_origin loc  -- After applying an instance we can set ScOrigin to
+                     -- infinity, so that prohibitedSuperClassSolve never fires
+       | ScOrigin {} <- origin
+       = setCtLocOrigin loc (ScOrigin infinity)
+       | otherwise
+       = loc
+
 {- Note [Instances in no-evidence implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In Trac #15290 we had
@@ -2331,40 +2328,10 @@ This test arranges to ignore the instance-based solution under these
 (rare) circumstances.   It's sad, but I  really don't see what else we can do.
 -}
 
-{- *******************************************************************
-*                                                                    *
-                       Class lookup
-*                                                                    *
-**********************************************************************-}
-
--- | Indicates if Instance met the Safe Haskell overlapping instances safety
--- check.
---
--- See Note [Safe Haskell Overlapping Instances] in TcSimplify
--- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
-type SafeOverlapping = Bool
-
-data LookupInstResult
-  = NoInstance   -- Definitely no instance
-
-  | OneInst { lir_new_theta :: [TcPredType]
-            , lir_mk_ev     :: [EvExpr] -> EvTerm
-            , lir_safe_over :: SafeOverlapping }
-
-  | NotSure      -- Multiple matches and/or one or more unifiers
-
-instance Outputable LookupInstResult where
-  ppr NoInstance = text "NoInstance"
-  ppr NotSure    = text "NotSure"
-  ppr (OneInst { lir_new_theta = ev
-               , lir_safe_over = s })
-    = text "OneInst" <+> vcat [ppr ev, ss]
-    where ss = text $ if s then "[safe]" else "[unsafe]"
-
 
 matchClassInst :: DynFlags -> InertSet
                -> Class -> [Type]
-               -> CtLoc -> TcS LookupInstResult
+               -> CtLoc -> TcS ClsInstResult
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
 -- match this constraint.  In that case, do not use any instance
@@ -2393,28 +2360,12 @@ matchClassInst dflags inerts clas tys loc
                    ; return local_res }
 
            NoInstance  -- No local instances, so try global ones
-              -> do { global_res <- matchGlobalInst dflags False clas tys loc
+              -> do { global_res <- matchGlobalInst dflags False clas tys
                     ; traceTcS "} matchClassInst global result" $ ppr global_res
                     ; return global_res } }
   where
     pred = mkClassPred clas tys
 
-matchGlobalInst :: DynFlags
-                -> Bool      -- True <=> caller is the short-cut solver
-                             -- See Note [Shortcut solving: overlap]
-                -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchGlobalInst dflags short_cut clas tys loc
-  | cls_name == knownNatClassName     = matchKnownNat        clas tys
-  | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
-  | isCTupleClass clas                = matchCTuple          clas tys
-  | cls_name == typeableClassName     = matchTypeable        clas tys
-  | clas `hasKey` heqTyConKey         = matchLiftedEquality       tys
-  | clas `hasKey` coercibleTyConKey   = matchLiftedCoercible      tys
-  | cls_name == hasFieldClassName     = matchHasField dflags short_cut clas tys loc
-  | otherwise                         = matchInstEnv dflags short_cut clas tys loc
-  where
-    cls_name = className clas
-
 -- | If a class is "naturally coherent", then we needn't worry at all, in any
 -- way, about overlapping/incoherent instances. Just solve the thing!
 -- See Note [Naturally coherent classes]
@@ -2581,7 +2532,7 @@ those instances to build evidence to pass to f. That's just the
 nullary case of what's happening here.
 -}
 
-matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult
+matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
 -- Try any Given quantified constraints, which are
 -- effectively just local instance declarations.
 matchLocalInst pred loc
@@ -2590,7 +2541,11 @@ matchLocalInst pred loc
            ([], False) -> return NoInstance
            ([(dfun_ev, inst_tys)], unifs)
              | not unifs
-             -> match_one pred loc True (ctEvEvId dfun_ev) inst_tys
+             -> do { let dfun_id = ctEvEvId dfun_ev
+                   ; (tys, theta) <- instDFunType dfun_id inst_tys
+                   ; return $ OneInst { cir_new_theta = theta
+                                      , cir_mk_ev     = evDFunApp dfun_id tys
+                                      , cir_what      = LocalInstance } }
            _ -> return NotSure }
   where
     pred_tv_set = tyCoVarsOfType pred
@@ -2620,478 +2575,3 @@ matchLocalInst pred loc
         this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
         (matches, unif) = match_local_inst qcis
 
-matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchInstEnv dflags short_cut_solver clas tys loc
-   = do { instEnvs <- getInstEnvs
-        ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
-              (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
-              safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
-        ; traceTcS "matchInstEnv" $
-            vcat [ text "goal:" <+> ppr clas <+> ppr tys
-                 , text "matches:" <+> ppr matches
-                 , text "unify:" <+> ppr unify ]
-        ; case (matches, unify, safeHaskFail) of
-
-            -- Nothing matches
-            ([], [], _)
-                -> do { traceTcS "matchClass not matching" (ppr pred)
-                      ; return NoInstance }
-
-            -- A single match (& no safe haskell failure)
-            ([(ispec, inst_tys)], [], False)
-                | short_cut_solver      -- Called from the short-cut solver
-                , isOverlappable ispec
-                -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
-                -- then don't let the short-cut solver choose it, because a
-                -- later instance might overlap it.  Trac #14434 is an example
-                -- See Note [Shortcut solving: overlap]
-                -> do { traceTcS "matchClass: ignoring overlappable" (ppr pred)
-                      ; return NotSure }
-
-                | otherwise
-                -> do { let dfun_id = instanceDFunId ispec
-                      ; traceTcS "matchClass success" $
-                        vcat [text "dict" <+> ppr pred,
-                              text "witness" <+> ppr dfun_id
-                                             <+> ppr (idType dfun_id) ]
-                                -- Record that this dfun is needed
-                      ; match_one pred loc (null unsafeOverlaps) dfun_id inst_tys }
-
-            -- More than one matches (or Safe Haskell fail!). Defer any
-            -- reactions of a multitude until we learn more about the reagent
-            _   -> do { traceTcS "matchClass multiple matches, deferring choice" $
-                        vcat [text "dict" <+> ppr pred,
-                              text "matches" <+> ppr matches]
-                      ; return NotSure } }
-   where
-     pred = mkClassPred clas tys
-
-match_one :: TcPredType -> CtLoc -> SafeOverlapping
-          -> DFunId -> [DFunInstType] -> TcS LookupInstResult
-             -- See Note [DFunInstType: instantiating types] in InstEnv
-match_one pred loc so dfun_id mb_inst_tys
-  = do { traceTcS "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
-       ; checkWellStagedDFun pred dfun_id loc
-       ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
-       ; traceTcS "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
-       ; return $ OneInst { lir_new_theta = theta
-                          , lir_mk_ev     = evDFunApp dfun_id tys
-                          , lir_safe_over = so } }
-
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for CTuples
-*                                                                     *
-***********************************************************************-}
-
-matchCTuple :: Class -> [Type] -> TcS LookupInstResult
-matchCTuple clas tys   -- (isCTupleClass clas) holds
-  = return (OneInst { lir_new_theta = tys
-                    , lir_mk_ev     = tuple_ev
-                    , lir_safe_over = True })
-            -- The dfun *is* the data constructor!
-  where
-     data_con = tyConSingleDataCon (classTyCon clas)
-     tuple_ev = evDFunApp (dataConWrapId data_con) tys
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Literals
-*                                                                     *
-***********************************************************************-}
-
-{-
-Note [KnownNat & KnownSymbol and EvLit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A part of the type-level literals implementation are the classes
-"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
-defining singleton values.  Here is the key stuff from GHC.TypeLits
-
-  class KnownNat (n :: Nat) where
-    natSing :: SNat n
-
-  newtype SNat (n :: Nat) = SNat Integer
-
-Conceptually, this class has infinitely many instances:
-
-  instance KnownNat 0       where natSing = SNat 0
-  instance KnownNat 1       where natSing = SNat 1
-  instance KnownNat 2       where natSing = SNat 2
-  ...
-
-In practice, we solve `KnownNat` predicates in the type-checker
-(see typecheck/TcInteract.hs) because we can't have infinitely many instances.
-The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
-
-We make the following assumptions about dictionaries in GHC:
-  1. The "dictionary" for classes with a single method---like `KnownNat`---is
-     a newtype for the type of the method, so using a evidence amounts
-     to a coercion, and
-  2. Newtypes use the same representation as their definition types.
-
-So, the evidence for `KnownNat` is just a value of the representation type,
-wrapped in two newtype constructors: one to make it into a `SNat` value,
-and another to make it into a `KnownNat` dictionary.
-
-Also note that `natSing` and `SNat` are never actually exposed from the
-library---they are just an implementation detail.  Instead, users see
-a more convenient function, defined in terms of `natSing`:
-
-  natVal :: KnownNat n => proxy n -> Integer
-
-The reason we don't use this directly in the class is that it is simpler
-and more efficient to pass around an integer rather than an entire function,
-especially when the `KnowNat` evidence is packaged up in an existential.
-
-The story for kind `Symbol` is analogous:
-  * class KnownSymbol
-  * newtype SSymbol
-  * Evidence: a Core literal (e.g. mkNaturalExpr)
--}
-
-matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
-matchKnownNat clas [ty]     -- clas = KnownNat
-  | Just n <- isNumLitTy ty = do
-        et <- mkNaturalExpr n
-        makeLitDict clas ty et
-matchKnownNat _ _           = return NoInstance
-
-matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
-matchKnownSymbol clas [ty]  -- clas = KnownSymbol
-  | Just s <- isStrLitTy ty = do
-        et <- mkStringExprFS s
-        makeLitDict clas ty et
-matchKnownSymbol _ _       = return NoInstance
-
-makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult
--- makeLitDict adds a coercion that will convert the literal into a dictionary
--- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
--- in TcEvidence.  The coercion happens in 2 steps:
---
---     Integer -> SNat n     -- representation of literal to singleton
---     SNat n  -> KnownNat n -- singleton to dictionary
---
---     The process is mirrored for Symbols:
---     String    -> SSymbol n
---     SSymbol n -> KnownSymbol n
-makeLitDict clas ty et
-    | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
-          -- co_dict :: KnownNat n ~ SNat n
-    , [ meth ]   <- classMethods clas
-    , Just tcRep <- tyConAppTyCon_maybe -- SNat
-                      $ funResultTy         -- SNat n
-                      $ dropForAlls         -- KnownNat n => SNat n
-                      $ idType meth         -- forall n. KnownNat n => SNat n
-    , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
-          -- SNat n ~ Integer
-    , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
-    = return $ OneInst { lir_new_theta = []
-                       , lir_mk_ev     = \_ -> ev_tm
-                       , lir_safe_over = True }
-
-    | otherwise
-    = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
-                     $$ vcat (map (ppr . idType) (classMethods clas)))
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Typeable
-*                                                                     *
-***********************************************************************-}
-
--- | Assumes that we've checked that this is the 'Typeable' class,
--- and it was applied to the correct argument.
-matchTypeable :: Class -> [Type] -> TcS LookupInstResult
-matchTypeable clas [k,t]  -- clas = Typeable
-  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
-  | isForAllTy k                      = return NoInstance   -- Polytype
-  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
-
-  -- Now cases that do work
-  | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
-  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
-  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
-  | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
-  | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
-  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
-  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
-
-matchTypeable _ _ = return NoInstance
-
--- | Representation for a type @ty@ of the form @arg -> ret@.
-doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
-doFunTy clas ty arg_ty ret_ty
-  = return $ OneInst { lir_new_theta = preds
-                     , lir_mk_ev     = mk_ev
-                     , lir_safe_over = True }
-  where
-    preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
-    mk_ev [arg_ev, ret_ev] = evTypeable ty $
-                             EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
-    mk_ev _ = panic "TcInteract.doFunTy"
-
-
--- | Representation for type constructor applied to some kinds.
--- 'onlyNamedBndrsApplied' has ensured that this application results in a type
--- of monomorphic kind (e.g. all kind variables have been instantiated).
-doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
-doTyConApp clas ty tc kind_args
-  | Just _ <- tyConRepName_maybe tc
-  = return $ OneInst { lir_new_theta = (map (mk_typeable_pred clas) kind_args)
-                     , lir_mk_ev = mk_ev
-                     , lir_safe_over = True }
-  | otherwise
-  = return NoInstance
-  where
-    mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
-
--- | Representation for TyCon applications of a concrete kind. We just use the
--- kind itself, but first we must make sure that we've instantiated all kind-
--- polymorphism, but no more.
-onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
-onlyNamedBndrsApplied tc ks
- = all isNamedTyConBinder used_bndrs &&
-   not (any isNamedTyConBinder leftover_bndrs)
- where
-   bndrs                        = tyConBinders tc
-   (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
-
-doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
--- Representation for an application of a type to a type-or-kind.
---  This may happen when the type expression starts with a type variable.
---  Example (ignoring kind parameter):
---    Typeable (f Int Char)                      -->
---    (Typeable (f Int), Typeable Char)          -->
---    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
---    Typeable f
-doTyApp clas ty f tk
-  | isForAllTy (typeKind f)
-  = return NoInstance -- We can't solve until we know the ctr.
-  | otherwise
-  = return $ OneInst { lir_new_theta = map (mk_typeable_pred clas) [f, tk]
-                     , lir_mk_ev     = mk_ev
-                     , lir_safe_over = True }
-  where
-    mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
-    mk_ev _ = panic "doTyApp"
-
-
--- Emit a `Typeable` constraint for the given type.
-mk_typeable_pred :: Class -> Type -> PredType
-mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
-
-  -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
-  -- we generate a sub-goal for the appropriate class.
-  -- See Note [Typeable for Nat and Symbol]
-doTyLit :: Name -> Type -> TcS LookupInstResult
-doTyLit kc t = do { kc_clas <- tcLookupClass kc
-                  ; let kc_pred    = mkClassPred kc_clas [ t ]
-                        mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
-                        mk_ev _    = panic "doTyLit"
-                  ; return (OneInst { lir_new_theta = [kc_pred]
-                                    , lir_mk_ev     = mk_ev
-                                    , lir_safe_over   = True }) }
-
-{- Note [Typeable (T a b c)]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For type applications we always decompose using binary application,
-via doTyApp, until we get to a *kind* instantiation.  Example
-   Proxy :: forall k. k -> *
-
-To solve Typeable (Proxy (* -> *) Maybe) we
-  - First decompose with doTyApp,
-    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
-  - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
-
-If we attempt to short-cut by solving it all at once, via
-doTyConApp
-
-(this note is sadly truncated FIXME)
-
-
-Note [No Typeable for polytypes or qualified types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not support impredicative typeable, such as
-   Typeable (forall a. a->a)
-   Typeable (Eq a => a -> a)
-   Typeable (() => Int)
-   Typeable (((),()) => Int)
-
-See Trac #9858.  For forall's the case is clear: we simply don't have
-a TypeRep for them.  For qualified but not polymorphic types, like
-(Eq a => a -> a), things are murkier.  But:
-
- * We don't need a TypeRep for these things.  TypeReps are for
-   monotypes only.
-
- * Perhaps we could treat `=>` as another type constructor for `Typeable`
-   purposes, and thus support things like `Eq Int => Int`, however,
-   at the current state of affairs this would be an odd exception as
-   no other class works with impredicative types.
-   For now we leave it off, until we have a better story for impredicativity.
-
-
-Note [Typeable for Nat and Symbol]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We have special Typeable instances for Nat and Symbol.  Roughly we
-have this instance, implemented here by doTyLit:
-      instance KnownNat n => Typeable (n :: Nat) where
-         typeRep = tyepNatTypeRep @n
-where
-   Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a
-
-Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
-runtime value 'n'; it turns it into a string with 'show' and uses
-that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
-See #10348.
-
-Because of this rule it's inadvisable (see #15322) to have a constraint
-    f :: (Typeable (n :: Nat)) => blah
-in a function signature; it gives rise to overlap problems just as
-if you'd written
-    f :: Eq [a] => blah
--}
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for lifted equality
-*                                                                     *
-***********************************************************************-}
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedEquality :: [Type] -> TcS LookupInstResult
-matchLiftedEquality args
-  = return (OneInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , lir_mk_ev     = evDFunApp (dataConWrapId heqDataCon) args
-                    , lir_safe_over = True })
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedCoercible :: [Type] -> TcS LookupInstResult
-matchLiftedCoercible args@[k, t1, t2]
-  = return (OneInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , lir_mk_ev     = evDFunApp (dataConWrapId coercibleDataCon)
-                                                args
-                    , lir_safe_over = True })
-  where
-    args' = [k, k, t1, t2]
-matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
-
-
-{- ********************************************************************
-*                                                                     *
-              Class lookup for overloaded record fields
-*                                                                     *
-***********************************************************************-}
-
-{-
-Note [HasField instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
-    data T y = MkT { foo :: [y] }
-
-and `foo` is in scope.  Then GHC will automatically solve a constraint like
-
-    HasField "foo" (T Int) b
-
-by emitting a new wanted
-
-    T alpha -> [alpha] ~# T Int -> b
-
-and building a HasField dictionary out of the selector function `foo`,
-appropriately cast.
-
-The HasField class is defined (in GHC.Records) thus:
-
-    class HasField (x :: k) r a | x r -> a where
-      getField :: r -> a
-
-Since this is a one-method class, it is represented as a newtype.
-Hence we can solve `HasField "foo" (T Int) b` by taking an expression
-of type `T Int -> b` and casting it using the newtype coercion.
-Note that
-
-    foo :: forall y . T y -> [y]
-
-so the expression we construct is
-
-    foo @alpha |> co
-
-where
-
-    co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
-
-is built from
-
-    co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
-
-which is the new wanted, and
-
-    co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
-
-which can be derived from the newtype coercion.
-
-If `foo` is not in scope, or has a higher-rank or existentially
-quantified type, then the constraint is not solved automatically, but
-may be solved by a user-supplied HasField instance.  Similarly, if we
-encounter a HasField constraint where the field is not a literal
-string, or does not belong to the type, then we fall back on the
-normal constraint solver behaviour.
--}
-
--- See Note [HasField instances]
-matchHasField :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchHasField dflags short_cut clas tys loc
-  = do { fam_inst_envs <- getFamInstEnvs
-       ; rdr_env       <- getGlobalRdrEnvTcS
-       ; case tys of
-           -- We are matching HasField {k} x r a...
-           [_k_ty, x_ty, r_ty, a_ty]
-               -- x should be a literal string
-             | Just x <- isStrLitTy x_ty
-               -- r should be an applied type constructor
-             , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
-               -- use representation tycon (if data family); it has the fields
-             , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
-               -- x should be a field of r
-             , Just fl <- lookupTyConFieldLabel x r_tc
-               -- the field selector should be in scope
-             , Just gre <- lookupGRE_FieldLabel rdr_env fl
-
-             -> do { sel_id <- tcLookupId (flSelector fl)
-                   ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
-
-                         -- The first new wanted constraint equates the actual
-                         -- type of the selector with the type (r -> a) within
-                         -- the HasField x r a dictionary.  The preds will
-                         -- typically be empty, but if the datatype has a
-                         -- "stupid theta" then we have to include it here.
-                   ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
-
-                         -- Use the equality proof to cast the selector Id to
-                         -- type (r -> a), then use the newtype coercion to cast
-                         -- it to a HasField dictionary.
-                         mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
-                           where
-                             co = mkTcSubCo (evTermCoercion (EvExpr ev1))
-                                      `mkTcTransCo` mkTcSymCo co2
-                         mk_ev [] = panic "matchHasField.mk_ev"
-
-                         Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
-                                                              tys
-
-                         tvs = mkTyVarTys (map snd tv_prs)
-
-                     -- The selector must not be "naughty" (i.e. the field
-                     -- cannot have an existentially quantified type), and
-                     -- it must not be higher-rank.
-                   ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
-                     then do { addUsedGRE True gre
-                             ; return OneInst { lir_new_theta = theta
-                                              , lir_mk_ev     = mk_ev
-                                              , lir_safe_over = True
-                                              } }
-                     else matchInstEnv dflags short_cut clas tys loc }
-
-           _ -> matchInstEnv dflags short_cut clas tys loc }
index 0ac91a1..3f0db9c 100644 (file)
@@ -20,6 +20,7 @@ module TcSMonad (
     checkConstraintsTcS, checkTvConstraintsTcS,
 
     runTcPluginTcS, addUsedGRE, addUsedGREs,
+    matchGlobalInst, TcM.ClsInstResult(..),
 
     QCInst(..),
 
@@ -97,7 +98,7 @@ module TcSMonad (
     -- MetaTyVars
     newFlexiTcSTy, instFlexi, instFlexiX,
     cloneMetaTyVar, demoteUnfilledFmv,
-    tcInstType, tcInstSkolTyVarsX,
+    tcInstSkolTyVarsX,
 
     TcLevel,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
@@ -107,7 +108,7 @@ module TcSMonad (
     zonkTcTyCoVarBndr,
 
     -- References
-    newTcRef, readTcRef, updTcRef,
+    newTcRef, readTcRef, writeTcRef, updTcRef,
 
     -- Misc
     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
@@ -133,9 +134,11 @@ import FamInstEnv
 
 import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
+import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) )
 import qualified TcEnv as TcM
-       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass, tcLookupId )
+       ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
 import PrelNames( heqTyConKey, eqTyConKey )
+import ClsInst( InstanceWhat(..) )
 import Kind
 import TcType
 import DynFlags
@@ -363,13 +366,13 @@ selectNextWorkItem :: TcS (Maybe Ct)
 -- See Note [Prioritise equalities]
 selectNextWorkItem
   = do { wl_var <- getTcSWorkListRef
-       ; wl <- wrapTcS (TcM.readTcRef wl_var)
+       ; wl <- readTcRef wl_var
        ; case selectWorkItem wl of {
            Nothing -> return Nothing ;
            Just (ct, new_wl) ->
     do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
          -- This is done by TcInteract.chooseInstance
-       ; wrapTcS (TcM.writeTcRef wl_var new_wl)
+       ; writeTcRef wl_var new_wl
        ; return (Just ct) } } }
 
 -- Pretty printing
@@ -2927,21 +2930,21 @@ getTcSWorkListRef :: TcS (IORef WorkList)
 getTcSWorkListRef = TcS (return . tcs_worklist)
 
 getTcSInerts :: TcS InertSet
-getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
+getTcSInerts = getTcSInertsRef >>= readTcRef
 
 setTcSInerts :: InertSet -> TcS ()
-setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
+setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics }
 
 getWorkListImplics :: TcS (Bag Implication)
 getWorkListImplics
   = do { wl_var <- getTcSWorkListRef
-       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
+       ; wl_curr <- readTcRef wl_var
        ; return (wl_implics wl_curr) }
 
 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
 updWorkListTcS f
   = do { wl_var <- getTcSWorkListRef
-       ; wrapTcS (TcM.updTcRef wl_var f)}
+       ; updTcRef wl_var f }
 
 emitWorkNC :: [CtEvidence] -> TcS ()
 emitWorkNC evs
@@ -2961,6 +2964,9 @@ newTcRef x = wrapTcS (TcM.newTcRef x)
 readTcRef :: TcRef a -> TcS a
 readTcRef ref = wrapTcS (TcM.readTcRef ref)
 
+writeTcRef :: TcRef a -> a -> TcS ()
+writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val)
+
 updTcRef :: TcRef a -> (a->a) -> TcS ()
 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
 
@@ -3043,14 +3049,24 @@ addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
-checkWellStagedDFun pred dfun_id loc
+checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
+-- Check that we do not try to use an instance before it is available.  E.g.
+--    instance Eq T where ...
+--    f x = $( ... (\(p::T) -> p == p)... )
+-- Here we can't use the equality function from the instance in the splice
+
+checkWellStagedDFun loc what pred
+  | TopLevInstance { iw_dfun_id = dfun_id } <- what
+  , let bind_lvl = TcM.topIdLvl dfun_id
+  , bind_lvl > impLevel
   = wrapTcS $ TcM.setCtLocM loc $
     do { use_stage <- TcM.getStage
        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
+
+  | otherwise
+  = return ()    -- Fast path for common case
   where
     pp_thing = text "instance for" <+> quotes (ppr pred)
-    bind_lvl = TcM.topIdLvl dfun_id
 
 pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
@@ -3059,7 +3075,7 @@ isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
 isFilledMetaTyVar_maybe tv
  = case tcTyVarDetails tv of
      MetaTv { mtv_ref = ref }
-        -> do { cts <- wrapTcS (TcM.readTcRef ref)
+        -> do { cts <- readTcRef ref
               ; case cts of
                   Indirect ty -> return (Just ty)
                   Flexi       -> return Nothing }
@@ -3268,12 +3284,12 @@ instFlexiHelper subst tv
        ; TcM.traceTc "instFlexi" (ppr ty')
        ; return (extendTvSubst subst tv ty') }
 
-tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-                   -- ^ How to instantiate the type variables
-           -> Id   -- ^ Type to instantiate
-           -> TcS ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
-                -- (type vars, preds (incl equalities), rho)
-tcInstType inst_tyvars id = wrapTcS (TcM.tcInstType inst_tyvars id)
+matchGlobalInst :: DynFlags
+                -> Bool      -- True <=> caller is the short-cut solver
+                             -- See Note [Shortcut solving: overlap]
+                -> Class -> [Type] -> TcS TcM.ClsInstResult
+matchGlobalInst dflags short_cut cls tys
+  = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
 
 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
 tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
index c504ad9..8f9b72b 100644 (file)
@@ -410,7 +410,7 @@ How is this implemented? It's complicated! So we'll step through it all:
     the list is null.
 
  2) `TcInteract.matchClassInst` -- This module drives the instance resolution
-    / dictionary generation. The return type is `LookupInstResult`, which either
+    / dictionary generation. The return type is `ClsInstResult`, which either
     says no instance matched, or one found, and if it was a safe or unsafe
     overlap.
 
index 0dc5664..86cb922 100644 (file)
@@ -27,6 +27,7 @@ import Maybes
 -- friends:
 import TcUnify    ( tcSubType_NC )
 import TcSimplify ( simplifyAmbiguityCheck )
+import ClsInst    ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..) )
 import TyCoRep
 import TcType hiding ( sizeType, sizeTypes )
 import PrelNames
@@ -40,15 +41,15 @@ import TyCon
 -- others:
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
-import TcEnv       ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv )
+import TcEnv       ( tcInitTidyEnv, tcInitOpenTidyEnv )
 import FunDeps
-import InstEnv     ( InstMatch, lookupInstEnv )
 import FamInstEnv  ( isDominatedBy, injectiveBranches,
                      InjectivityCheckResult(..) )
 import FamInst     ( makeInjectivityErrors )
 import Name
 import VarEnv
 import VarSet
+import Id          ( idType, idName )
 import Var         ( TyVarBndr(..), mkTyVar )
 import ErrUtils
 import DynFlags
@@ -680,9 +681,9 @@ applying the instance decl would show up two uses of ?x.  Trac #8912.
 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
 -- Assumes argument is fully zonked
 checkValidTheta ctxt theta
-  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
-       ; addErrCtxtM (checkThetaCtxt ctxt theta) $
-         check_valid_theta env ctxt theta }
+  = addErrCtxtM (checkThetaCtxt ctxt theta) $
+    do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
+       ; check_valid_theta env ctxt theta }
 
 -------------------------
 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
@@ -748,32 +749,47 @@ check_pred_help under_syn env dflags ctxt pred
 
   | otherwise  -- A bit like classifyPredType, but not the same
                -- E.g. we treat (~) like (~#); and we look inside tuples
-  = case splitTyConApp_maybe pred of
-      Just (tc, tys)
-        | isTupleTyCon tc
-        -> check_tuple_pred under_syn env dflags ctxt pred tys
-
-        | tc `hasKey` heqTyConKey ||
-          tc `hasKey` eqTyConKey ||
-          tc `hasKey` eqPrimTyConKey
-          -- NB: this equality check must come first,
-          --  because (~) is a class,too.
-        -> check_eq_pred env dflags pred tc tys
-
-        | Just cls <- tyConClass_maybe tc
-          -- Includes Coercible
-        -> check_class_pred env dflags ctxt pred cls tys
-
-      _ -> check_irred_pred under_syn env dflags ctxt pred
-
-check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
-check_eq_pred env dflags pred tc tys
+  = case classifyPredType pred of
+      ClassPred cls tys
+        | isCTupleClass cls   -> check_tuple_pred under_syn env dflags ctxt pred tys
+        | otherwise           -> check_class_pred env dflags ctxt pred cls tys
+
+      EqPred NomEq _ _  -> -- a ~# b
+                           check_eq_pred env dflags pred
+
+      EqPred ReprEq _ _ -> -- Ugh!  When inferring types we may get
+                           -- f :: (a ~R# b) => blha
+                           -- And we want to treat that like (Coercible a b)
+                           -- We should probably check argument shapes, but we
+                           -- didn't do so before, so I'm leaving it for now
+                           return ()
+
+      ForAllPred _ theta head -> check_quant_pred env dflags pred theta head
+      IrredPred {}            -> check_irred_pred under_syn env dflags ctxt pred
+
+check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
+check_eq_pred env dflags pred
   =         -- Equational constraints are valid in all contexts if type
             -- families are permitted
-    do { checkTc (tys `lengthIs` tyConArity tc) (tyConArityErr tc tys)
-       ; checkTcM (xopt LangExt.TypeFamilies dflags
-                   || xopt LangExt.GADTs dflags)
-                  (eqPredTyErr env pred) }
+    checkTcM (xopt LangExt.TypeFamilies dflags
+              || xopt LangExt.GADTs dflags)
+             (eqPredTyErr env pred)
+
+check_quant_pred :: TidyEnv -> DynFlags -> PredType
+                 -> ThetaType -> PredType -> TcM ()
+check_quant_pred env dflags pred theta head_pred
+  = addErrCtxt (text "In the quantified constraint"
+                <+> quotes (ppr pred)) $
+    do { checkTcM head_ok (badQuantHeadErr env pred)
+
+       ; unless (xopt LangExt.UndecidableInstances dflags) $
+         checkInstTermination theta head_pred
+    }
+  where
+    head_ok = case classifyPredType head_pred of
+                 ClassPred {} -> True
+                 IrredPred {} -> hasTyVarHead head_pred
+                 _            -> False
 
 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
 check_tuple_pred under_syn env dflags ctxt pred ts
@@ -833,16 +849,21 @@ This will cause the constraint simplifier to loop because every time we canonica
 solved to add+canonicalise another (Foo a) constraint.  -}
 
 -------------------------
-check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
+check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
+                 -> PredType -> Class -> [TcType] -> TcM ()
 check_class_pred env dflags ctxt pred cls tys
+  |  cls `hasKey` heqTyConKey   -- (~) and (~~) are classified as classes,
+  || cls `hasKey` eqTyConKey    -- but here we want to treat them as equalities
+  = pprTrace "check_class" (ppr cls) $
+    check_eq_pred env dflags pred
+
   | isIPClass cls
   = do { check_arity
        ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
 
-  | otherwise
+  | otherwise     -- Includes Coercible
   = do { check_arity
-       ; warn_simp <- woptM Opt_WarnSimplifiableClassConstraints
-       ; when warn_simp check_simplifiable_class_constraint
+       ; checkSimplifiableClassConstraint env dflags ctxt cls tys
        ; checkTcM arg_tys_ok (predTyVarErr env pred) }
   where
     check_arity = checkTc (tys `lengthIs` classArity cls)
@@ -858,27 +879,48 @@ check_class_pred env dflags ctxt pred cls tys
                                 -- in checkInstTermination
         _            -> checkValidClsArgs flexible_contexts cls tys
 
-    -- See Note [Simplifiable given constraints]
-    check_simplifiable_class_constraint
-       | xopt LangExt.MonoLocalBinds dflags
-       = return ()
-       | DataTyCtxt {} <- ctxt   -- Don't do this check for the "stupid theta"
-       = return ()               -- of a data type declaration
-       | otherwise
-       = do { envs <- tcGetInstEnvs
-            ; case lookupInstEnv False envs cls tys of
-                 ([m], [], _) -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
-                                           (simplifiable_constraint_warn m)
-                 _ -> return () }
-
-    simplifiable_constraint_warn :: InstMatch -> SDoc
-    simplifiable_constraint_warn (match, _)
-     = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
-                 2 (text "matches an instance declaration")
-            , ppr match
+checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
+                                 -> Class -> [TcType] -> TcM ()
+-- See Note [Simplifiable given constraints]
+checkSimplifiableClassConstraint env dflags ctxt cls tys
+  | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
+  = return ()
+  | xopt LangExt.MonoLocalBinds dflags
+  = return ()
+
+  | DataTyCtxt {} <- ctxt   -- Don't do this check for the "stupid theta"
+  = return ()               -- of a data type declaration
+
+  | cls `hasKey` coercibleTyConKey
+  = return ()   -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
+                -- matchGlobalInst will reply "yes" because we can reduce
+                -- (Coercible a b) to (a ~R# b)
+
+  | otherwise
+  = do { result <- matchGlobalInst dflags False cls tys
+       ; case result of
+           OneInst { cir_what = what }
+              -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
+                                   (simplifiable_constraint_warn what)
+           _          -> return () }
+  where
+    pred = mkClassPred cls tys
+
+    simplifiable_constraint_warn :: InstanceWhat -> SDoc
+    simplifiable_constraint_warn what
+     = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
+                    <+> text "matches")
+                 2 (ppr_what what)
             , hang (text "This makes type inference for inner bindings fragile;")
                  2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
 
+    ppr_what BuiltinInstance = text "a built-in instance"
+    ppr_what LocalInstance   = text "a locally-quantified instance"
+    ppr_what (TopLevInstance { iw_dfun_id = dfun })
+      = hang (text "instance" <+> pprSigmaType (idType dfun))
+           2 (text "--" <+> pprDefinedAt (idName dfun))
+
+
 {- Note [Simplifiable given constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A type signature like
@@ -973,7 +1015,12 @@ checkThetaCtxt ctxt theta env
            , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
                   , text "While checking" <+> pprUserTypeCtxt ctxt ] )
 
-eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
+eqPredTyErr, predTupleErr, predIrredErr,
+   predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
+badQuantHeadErr env pred
+  = ( env
+    , hang (text "Quantified predicate must have a class or type variable head:")
+         2 (ppr_tidy env pred) )
 eqPredTyErr  env pred
   = ( env
     , text "Illegal equational constraint" <+> ppr_tidy env pred $$
@@ -1329,7 +1376,9 @@ checkValidInstance ctxt hs_type ty
   | otherwise
   = do  { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
         ; traceTc "checkValidInstance {" (ppr ty)
-        ; checkValidTheta ctxt theta
+
+        ; env0 <- tcInitTidyEnv
+        ; check_valid_theta env0 ctxt theta
 
         -- The Termination and Coverate Conditions
         -- Check that instance inference will terminate (if we care)
@@ -1415,16 +1464,15 @@ checkInstTermination theta head_pred
               bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
                                -- See Note [Invisible arguments and termination]
 
-         ForAllPred tvs theta' head_pred'
-           -> do { check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
-                 ; addErrCtxt (text "In the quantified constraint"
-                              <+> quotes (ppr pred)) $
-                   checkInstTermination theta' head_pred' }
+         ForAllPred tvs _ head_pred'
+           -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
+              -- Termination of the quantified predicate itself is checked
+              -- when the predicates are individually checked for validity
 
    check2 foralld_tvs pred pred_size
-     | not (null bad_tvs)     = addErrTc (noMoreMsg bad_tvs what (ppr head_pred))
-     | not (isTyFamFree pred) = addErrTc (nestedMsg what)
-     | pred_size >= head_size = addErrTc (smallerMsg what (ppr head_pred))
+     | not (null bad_tvs)     = failWithTc (noMoreMsg bad_tvs what (ppr head_pred))
+     | not (isTyFamFree pred) = failWithTc (nestedMsg what)
+     | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred))
      | otherwise              = return ()
      -- isTyFamFree: see Note [Type families in instance contexts]
      where
diff --git a/testsuite/tests/indexed-types/should_compile/T15322.hs b/testsuite/tests/indexed-types/should_compile/T15322.hs
new file mode 100644 (file)
index 0000000..5a0cd17
--- /dev/null
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module T15322 where
+
+import Data.Proxy (Proxy (..))
+import Type.Reflection
+import GHC.TypeLits (KnownNat, type (+))
+
+f :: forall n . (Typeable (n+1), KnownNat n) => Proxy n -> TypeRep (n+1)
+f _ = typeRep
diff --git a/testsuite/tests/indexed-types/should_compile/T15322.stderr b/testsuite/tests/indexed-types/should_compile/T15322.stderr
new file mode 100644 (file)
index 0000000..7447a9e
--- /dev/null
@@ -0,0 +1,8 @@
+
+T15322.hs:11:6: warning: [-Wsimplifiable-class-constraints (in -Wdefault)]
+    • The constraint ‘Typeable (n + 1)’ matches a built-in instance
+      This makes type inference for inner bindings fragile;
+        either use MonoLocalBinds, or simplify it using the instance
+    • In the type signature:
+        f :: forall n.
+             (Typeable (n + 1), KnownNat n) => Proxy n -> TypeRep (n + 1)
diff --git a/testsuite/tests/indexed-types/should_compile/T15322a.hs b/testsuite/tests/indexed-types/should_compile/T15322a.hs
new file mode 100644 (file)
index 0000000..93d0830
--- /dev/null
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module T15322a where
+
+import Data.Proxy (Proxy (..))
+import Type.Reflection
+import GHC.TypeLits (KnownNat, type (+))
+
+f :: forall n . (KnownNat n) => Proxy n -> TypeRep (n+1)
+f _ = typeRep
diff --git a/testsuite/tests/indexed-types/should_compile/T15322a.stderr b/testsuite/tests/indexed-types/should_compile/T15322a.stderr
new file mode 100644 (file)
index 0000000..37a9070
--- /dev/null
@@ -0,0 +1,12 @@
+
+T15322a.hs:12:7: error:
+    • Could not deduce (KnownNat (n + 1))
+        arising from a use of ‘typeRep’
+      from the context: KnownNat n
+        bound by the type signature for:
+                   f :: forall (n :: GHC.Types.Nat).
+                        KnownNat n =>
+                        Proxy n -> TypeRep (n + 1)
+        at T15322a.hs:11:1-56
+    • In the expression: typeRep
+      In an equation for ‘f’: f _ = typeRep
index 56448ac..6255dd2 100644 (file)
@@ -284,3 +284,5 @@ test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
 test('T14164', normal, compile, [''])
+test('T15322', normal, compile, [''])
+test('T15322a', normal, compile_fail, [''])
index 4b72ec4..262b76d 100644 (file)
@@ -7,8 +7,8 @@ Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
 
 SomethingShowable.hs:5:1: warning: [-Wsimplifiable-class-constraints (in -Wdefault)]
-    • The constraint ‘Show Bool’ matches an instance declaration
-      instance Show Bool -- Defined in ‘GHC.Show’
+    • The constraint ‘Show Bool’ matches
+        instance Show Bool -- Defined in ‘GHC.Show’
       This makes type inference for inner bindings fragile;
         either use MonoLocalBinds, or simplify it using the instance
     • When checking the inferred type
index f584731..616f317 100644 (file)
@@ -1,6 +1,4 @@
 
 T11466.hs:15:10: error:
     • Illegal implicit parameter ‘?x::Int’
-    • In the context: Bla
-      While checking an instance declaration
-      In the instance declaration for ‘Eq T’
+    • In the instance declaration for ‘Eq T’
diff --git a/testsuite/tests/quantified-constraints/T15316.hs b/testsuite/tests/quantified-constraints/T15316.hs
new file mode 100644 (file)
index 0000000..07539e3
--- /dev/null
@@ -0,0 +1,21 @@
+{-# LANGUAGE RankNTypes, QuantifiedConstraints, ConstraintKinds  #-}
+-- NB: disabling these if enabled:
+{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-}
+
+module T15316 where
+
+import Data.Proxy
+
+{-
+class Class a where
+         method :: a
+
+subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r
+subsume _ _ x = x
+
+value :: Proxy a -> a
+value p = subsume p p method
+-}
+
+subsume' :: Proxy c -> ((c => c) => r) -> r
+subsume' _ x = x
diff --git a/testsuite/tests/quantified-constraints/T15316.stderr b/testsuite/tests/quantified-constraints/T15316.stderr
new file mode 100644 (file)
index 0000000..4444c2c
--- /dev/null
@@ -0,0 +1,6 @@
+
+T15316.hs:20:13: error:
+    • The constraint ‘c’ is no smaller than the instance head ‘c’
+      (Use UndecidableInstances to permit this)
+    • In the quantified constraint ‘c => c’
+      In the type signature: subsume' :: Proxy c -> ((c => c) => r) -> r
index 65e6367..3145f47 100644 (file)
@@ -14,3 +14,4 @@ test('T15231', normal, compile_fail, [''])
 test('T15290', normal, compile, [''])
 test('T15290a', normal, compile_fail, [''])
 test('T15290b', normal, compile_fail, [''])
+test('T15316', normal, compile_fail, [''])
index fd84396..43aac8a 100644 (file)
@@ -1,5 +1,8 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
+    -- This test deliberately uses a simplifiable class constraint
+
 module T10177 where
 
 import Data.Typeable
index 7a0f2ae..ad5876e 100644 (file)
@@ -1,7 +1,7 @@
 
 T13526.hs:21:8: warning: [-Wsimplifiable-class-constraints (in -Wdefault)]
-    • The constraint ‘C (Maybe a)’ matches an instance declaration
-      instance C a => C (Maybe a) -- Defined at T13526.hs:14:10
+    • The constraint ‘C (Maybe a)’ matches
+        instance C a => C (Maybe a) -- Defined at T13526.hs:14:10
       This makes type inference for inner bindings fragile;
         either use MonoLocalBinds, or simplify it using the instance
     • In the type signature: bar :: C (Maybe a) => a -> Maybe a
index c401e1c..b5e20be 100644 (file)
@@ -13,11 +13,17 @@ using the solver (see `tcSuperClasses` in `TcInstDecls`).
 However, some classes need to be excepted from this behavior,
 as they have custom solving rules, and this test checks that
 we got this right.
+
+PS: this test used to have Typeable in the context too, but
+    that's a redundant constraint, so I removed it
+
+PPS: the whole structre of tcSuperClasses has changed,
+     so I'm no longer sure what is being tested here
 -}
 
 
-class (Typeable x, KnownNat x)    => C x
-class (Typeable x, KnownSymbol x) => D x
+class (KnownNat x)    => C x
+class (KnownSymbol x) => D x
 
 instance C 2
 instance D "2"
index bfe06c1..7d6f37d 100644 (file)
@@ -1,6 +1,4 @@
 
 T8912.hs:7:10: error:
     • Illegal implicit parameter ‘?imp::Int’
-    • In the context: ?imp::Int
-      While checking an instance declaration
-      In the instance declaration for ‘C [a]’
+    • In the instance declaration for ‘C [a]’
index 31fd91b..86a70f5 100644 (file)
@@ -4,9 +4,3 @@ fd-loop.hs:12:10: error:
         in the constraint ‘C a b’ than in the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
-
-fd-loop.hs:12:10: error:
-    • Variable ‘b’ occurs more often
-        in the constraint ‘Eq b’ than in the instance head ‘Eq (T a)’
-      (Use UndecidableInstances to permit this)
-    • In the instance declaration for ‘Eq (T a)’
index e81778c..4cb2af7 100644 (file)
@@ -5,10 +5,3 @@ tcfail157.hs:27:10: error:
         than in the instance head ‘Foo m (a -> ())’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Foo m (a -> ())’
-
-tcfail157.hs:27:10: error:
-    • Variable ‘b’ occurs more often
-        in the constraint ‘Foo m b’
-        than in the instance head ‘Foo m (a -> ())’
-      (Use UndecidableInstances to permit this)
-    • In the instance declaration for ‘Foo m (a -> ())’
index 7a5053a..fb1192b 100644 (file)
@@ -7,6 +7,4 @@ tcfail211.hs:5:1: error:
 
 tcfail211.hs:8:10: error:
     • Illegal implicit parameter ‘?imp::Int’
-    • In the context: ?imp::Int
-      While checking an instance declaration
-      In the instance declaration for ‘D Int’
+    • In the instance declaration for ‘D Int’