Yet another attempt at inferring the right quantification
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 5 Apr 2017 12:46:03 +0000 (13:46 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 6 Apr 2017 11:33:56 +0000 (12:33 +0100)
TcSimplify.decideQuantification is truly a tricky function!
Trac #13509 showed that we were being over-eager with defaulting
of runtime-rep variables (levity polymorphism), which meant that
a program was wrongly rejected, and with a very odd error message
(c.f. Trac #13530)

I spent an unreasonably long time figuring out how to fix this
in a decent way, and ended up with a major refactoring of
decideQuantification, with a kock-on effect in simplifyInfer.

It is at least a bit more comprehensible now; but I still
can't say I like it.

compiler/typecheck/TcMType.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
testsuite/tests/typecheck/should_compile/T13509.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 1f183ed..1a67875 100644 (file)
@@ -73,7 +73,7 @@ module TcMType (
   zonkTyCoVarsAndFV, zonkTcTypeAndFV,
   zonkTyCoVarsAndFVList,
   zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
-  zonkQuantifiedTyVar,
+  zonkQuantifiedTyVar, defaultTyVar,
   quantifyTyVars, quantifyZonkedTyVars,
   zonkTcTyCoVarBndr, zonkTcTyVarBinder,
   zonkTcType, zonkTcTypes, zonkCo,
@@ -960,12 +960,12 @@ quantifyZonkedTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
            -- mentioned in the kinds of the nondep_tvs'
            -- now refer to the dep_kvs'
 
-       ; traceTc "quantifyTyVars"
+       ; traceTc "quantifyZonkedTyVars"
            (vcat [ text "globals:" <+> ppr gbl_tvs
-                 , text "nondep:" <+> ppr nondep_tvs
-                 , text "dep:" <+> ppr dep_kvs
-                 , text "dep_kvs'" <+> ppr dep_kvs'
-                 , text "nondep_tvs'" <+> ppr nondep_tvs' ])
+                 , text "nondep:"  <+> pprTyVars nondep_tvs
+                 , text "dep:"     <+> pprTyVars dep_kvs
+                 , text "dep_kvs'" <+> pprTyVars dep_kvs'
+                 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
 
        ; return (dep_kvs' ++ nondep_tvs') }
   where
@@ -998,66 +998,59 @@ zonkQuantifiedTyVar :: Bool     -- True  <=> this is a kind var and -XNoPolyKind
 
 zonkQuantifiedTyVar default_kind tv
   = case tcTyVarDetails tv of
-      SkolemTv {} -> zonk_kind_and_return
+      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+                        ; return $ Just (setTyVarKind tv kind) }
         -- It might be a skolem type variable,
         -- for example from a user type signature
 
-      MetaTv { mtv_ref = ref, mtv_info = info }
-        -> do { when debugIsOn (check_empty ref)
-              ; zonk_meta_tv info tv }
+      MetaTv {}
+        -> do { mb_tv <- defaultTyVar default_kind tv
+              ; case mb_tv of
+                  True  -> return Nothing
+                  False -> do { tv' <- skolemiseUnboundMetaTyVar tv
+                              ; return (Just tv') } }
 
       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
 
-  where
-    zonk_kind_and_return = do { kind <- zonkTcType (tyVarKind tv)
-                              ; return $ Just (setTyVarKind tv kind) }
+defaultTyVar :: Bool      -- True <=> please default this kind variable to *
+             -> TcTyVar   -- Always an unbound meta tyvar
+             -> TcM Bool  -- True <=> defaulted away altogether
 
-    zonk_meta_tv :: MetaInfo -> TcTyVar -> TcM (Maybe TcTyVar)
-    zonk_meta_tv info tv
-      | isRuntimeRepVar tv && not_sig_tv  -- Never quantify over a RuntimeRep var
-      = do { writeMetaTyVar tv liftedRepTy
-           ; return Nothing }
+defaultTyVar default_kind tv
+  | isRuntimeRepVar tv && not_sig_tv  -- We never quantify over a RuntimeRep var
+  = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
+       ; writeMetaTyVar tv liftedRepTy
+       ; return True }
 
-      | default_kind && not_sig_tv        -- -XNoPolyKinds and this is a kind var
-      = do { _ <- default_kind_var tv
-           ; return Nothing }
+  | default_kind && not_sig_tv        -- -XNoPolyKinds and this is a kind var
+  = do { default_kind_var tv          -- so default it to * if possible
+       ; return True }
 
-      | otherwise
-      = do { tv' <- skolemiseUnboundMetaTyVar tv
-           ; return (Just tv') }
-      where
-        -- Do not default SigTvs. Doing so would violate the invariants
-        -- on SigTvs; see Note [Signature skolems] in TcType.
-        -- Trac #13343 is an example
-        not_sig_tv = case info of SigTv -> False
-                                  _     -> True
+  | otherwise
+  = return False
 
+  where
+    -- Do not default SigTvs. Doing so would violate the invariants
+    -- on SigTvs; see Note [Signature skolems] in TcType.
+    -- Trac #13343 is an example
+    not_sig_tv = not (isSigTyVar tv)
 
-    default_kind_var :: TyVar -> TcM Type
+    default_kind_var :: TyVar -> TcM ()
        -- defaultKindVar is used exclusively with -XNoPolyKinds
        -- See Note [Defaulting with -XNoPolyKinds]
        -- It takes an (unconstrained) meta tyvar and defaults it.
        -- Works only on vars of type *; for other kinds, it issues an error.
     default_kind_var kv
       | isStarKind (tyVarKind kv)
-      = do { writeMetaTyVar kv liftedTypeKind
-           ; return liftedTypeKind }
+      = do { traceTc "Defaulting a kind var to *" (ppr kv)
+           ; writeMetaTyVar kv liftedTypeKind }
       | otherwise
-      = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
-                          , text "of kind:" <+> ppr (tyVarKind kv')
-                          , text "Perhaps enable PolyKinds or add a kind signature" ])
-           ; return (mkTyVarTy kv) }
+      = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
+                     , text "of kind:" <+> ppr (tyVarKind kv')
+                     , text "Perhaps enable PolyKinds or add a kind signature" ])
       where
         (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
-    check_empty ref       -- [Sept 04] Check for non-empty.
-      = when debugIsOn $  -- See note [Silly Type Synonym]
-        do { cts <- readMutVar ref
-           ; case cts of
-               Flexi       -> return ()
-               Indirect ty -> WARN( True, ppr tv $$ ppr ty )
-                              return () }
-
 skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
 skolemiseRuntimeUnk tv
   = skolemise_tv tv RuntimeUnk
@@ -1074,7 +1067,8 @@ skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 --   See Note [Zonking to Skolem]
 skolemise_tv tv details
   = ASSERT2( isMetaTyVar tv, ppr tv )
-    do  { span <- getSrcSpanM    -- Get the location from "here"
+    do  { when debugIsOn (check_empty tv)
+        ; span <- getSrcSpanM    -- Get the location from "here"
                                  -- ie where we are generalising
         ; kind <- zonkTcType (tyVarKind tv)
         ; let uniq        = getUnique tv
@@ -1089,6 +1083,15 @@ skolemise_tv tv details
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
 
+  where
+    check_empty tv       -- [Sept 04] Check for non-empty.
+      = when debugIsOn $  -- See note [Silly Type Synonym]
+        do { cts <- readMetaTyVar tv
+           ; case cts of
+               Flexi       -> return ()
+               Indirect ty -> WARN( True, ppr tv $$ ppr ty )
+                              return () }
+
 {- Note [Defaulting with -XNoPolyKinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
index d3fd768..58830ec 100644 (file)
@@ -49,7 +49,7 @@ import BasicTypes    ( IntWithInf, intGtLimit )
 import ErrUtils      ( emptyMessages )
 import qualified GHC.LanguageExtensions as LangExt
 
-import Control.Monad ( when, unless )
+import Control.Monad
 import Data.List     ( partition )
 
 {-
@@ -626,47 +626,22 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        --      to less polymorphic types, see Note [Default while Inferring]
 
        ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
-       ; quant_pred_candidates   -- Fully zonked
-           <- if insolubleWC wanted_transformed_incl_derivs
-              then return []   -- See Note [Quantification with errors]
-                               -- NB: must include derived errors in this test,
-                               --     hence "incl_derivs"
-
-              else do { let quant_cand = approximateWC False wanted_transformed
-                            meta_tvs   = filter isMetaTyVar $
-                                         tyCoVarsOfCtsList quant_cand
-
-                      ; gbl_tvs <- tcGetGlobalTyCoVars
-                            -- Miminise quant_cand.  We are not interested in any evidence
-                            -- produced, because we are going to simplify wanted_transformed
-                            -- again later. All we want here are the predicates over which to
-                            -- quantify.
-                            --
-                            -- If any meta-tyvar unifications take place (unlikely),
-                            -- we'll pick that up later.
-
-                      -- See Note [Promote _and_ default when inferring]
-                      ; let def_tyvar tv
-                              = when (not $ tv `elemVarSet` gbl_tvs) $
-                                defaultTyVar tv
-                      ; mapM_ def_tyvar meta_tvs
-                      ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
-
-                      ; clone_wanteds <- mapM cloneWanted (bagToList quant_cand)
-                      ; WC { wc_simple = simples }
-                           <- setTcLevel rhs_tclvl $
-                              simplifyWantedsTcM clone_wanteds
-                              -- Discard evidence; result is zonked
-
-                      ; return [ ctEvPred ev | ct <- bagToList simples
-                                             , let ev = ctEvidence ct ] }
+             quant_pred_candidates   -- Fully zonked
+                 | insolubleWC wanted_transformed_incl_derivs
+                 = []   -- See Note [Quantification with errors]
+                        -- NB: must include derived errors in this test,
+                        --     hence "incl_derivs"
+
+                 | otherwise
+                 = ctsPreds (approximateWC False wanted_transformed)
 
        -- NB: quant_pred_candidates is already fully zonked
 
        -- Decide what type variables and constraints to quantify
        -- NB: bound_theta are constraints we want to quantify over,
        --     /apart from/ the psig_theta, which we always quantify over
-       ; (qtvs, bound_theta) <- decideQuantification infer_mode name_taus psig_theta
+       ; (qtvs, bound_theta) <- decideQuantification infer_mode rhs_tclvl
+                                                     name_taus psig_theta
                                                      quant_pred_candidates
 
          -- Promote any type variables that are free in the inferred type
@@ -753,6 +728,10 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                          Nothing -> add_psig_tvs qtvs      tvs
                          Just tv -> add_psig_tvs (tv:qtvs) tvs } }
 
+ctsPreds :: Cts -> [PredType]
+ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
+                             , let ev = ctEvidence ct ]
+
 {- Note [Add signature contexts as givens]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this (Trac #11016):
@@ -789,115 +768,205 @@ Note [Deciding quantification]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If the monomorphism restriction does not apply, then we quantify as follows:
 
-  * Take the global tyvars, and "grow" them using the equality constraints
-    E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
+* Step 1. Take the global tyvars, and "grow" them using the equality
+  constraints
+     E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
           happen because alpha is untouchable here) then do not quantify over
           beta, because alpha fixes beta, and beta is effectively free in
           the environment too
-    These are the mono_tvs
 
-  * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
-    using all the constraints.  These are tau_tvs_plus
+  We also account for the monomorphism restriction; if it applies,
+  add the free vars of all the constraints.
+
+  Result is mono_tvs; we will not quantify over these.
+
+* Step 2. Default any non-mono tyvars (i.e ones that are definitely
+  not going to become further constrained), and re-simplify the
+  candidate constraints.
+
+  Motivation for re-simplification (Trac #7857): imagine we have a
+  constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
+  not free in the envt, and instance forall (a::*) (b::*). (C a) => C
+  (a -> b) The instance doesnt' match while l1,l2 are polymorphic, but
+  it will match when we default them to LiftedRep.
+
+  This is all very tiresome.
 
-  * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
+* Step 3: decide which variables to quantify over, as follows:
+
+  - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
+    them using all the constraints.  These are tau_tvs_plus
+
+  - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
     careful to close over kinds, and to skolemise the quantified tyvars.
     (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
-    Result is qtvs.
 
-  * Filter the constraints using pickQuantifiablePreds and the qtvs.
-    We have to zonk the constraints first, so they "see" the freshly
-    created skolems.
+ Result is qtvs.
 
-If the MR does apply, mono_tvs includes all the constrained tyvars --
-including all covars -- and the quantified constraints are empty/insoluble.
+* Step 4: Filter the constraints using pickQuantifiablePreds and the
+  qtvs. We have to zonk the constraints first, so they "see" the
+  freshly created skolems.
 
 -}
 
 decideQuantification
   :: InferMode
+  -> TcLevel
   -> [(Name, TcTauType)]   -- Variables to be generalised
   -> [PredType]            -- All annotated constraints from signatures
   -> [PredType]            -- Candidate theta; already zonked
   -> TcM ( [TcTyVar]       -- Quantify over these (skolems)
          , [PredType] )    -- and this context (fully zonked)
 -- See Note [Deciding quantification]
-decideQuantification infer_mode name_taus psig_theta candidates
-  = do { ovl_strings <- xoptM LangExt.OverloadedStrings
-       ; gbl_tvs     <- tcGetGlobalTyCoVars
-       ; let (gbl_cand, quant_cand)    -- gbl_cand   = do not quantify me
-                = case infer_mode of   -- quant_cand = try to quantify me
-                    ApplyMR         -> (candidates, [])
-                    NoRestrictions  -> ([], candidates)
-                    EagerDefaulting -> partition is_interactive_ct candidates
-                      where
-                        is_interactive_ct ct
-                          | Just (cls, _) <- getClassPredTys_maybe ct
-                          = isInteractiveClass ovl_strings cls
-                          | otherwise
-                          = False
-
-             eq_constraints  = filter isEqPred quant_cand
-             constrained_tvs = tyCoVarsOfTypes gbl_cand
-             mono_tvs        = growThetaTyVars eq_constraints $
-                               gbl_tvs `unionVarSet` constrained_tvs
-
-       ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
-                        -- psig_theta: see Note [Quantification and partial signatures]
+decideQuantification infer_mode rhs_tclvl name_taus psig_theta candidates
+  = do { -- Step 1: find the mono_tvs
+         (mono_tvs, candidates) <- decideMonoTyVars infer_mode candidates name_taus
+
+       -- Step 2: default any non-mono tyvars, and re-simplify
+       ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+
+       -- Step 3: decide which kind/type variables to quantify over
+       ; qtvs <- decideQuantifiedTyVars mono_tvs candidates
+                                        psig_theta name_taus
+
+       -- Step 4: choose which of the remaining candidate
+       --         predicates to actually quantify over
+       -- NB: decideQuantifiedTyVars turned some meta tyvars
+       -- into quantified skolems, so we have to zonk again
+       ; candidates <- TcM.zonkTcTypes candidates
+       ; let theta = pickQuantifiablePreds (mkVarSet qtvs) $
+                     mkMinimalBySCs $  -- See Note [Minimize by Superclasses]
+                     candidates
+
+       ; traceTc "decideQuantification"
+           (vcat [ text "infer_mode:"   <+> ppr infer_mode
+                 , text "candidates:"   <+> ppr candidates
+                 , text "mono_tvs:"     <+> ppr mono_tvs
+                 , text "qtvs:"         <+> ppr qtvs
+                 , text "theta:"        <+> ppr theta ])
+       ; return (qtvs, theta) }
+
+------------------
+decideMonoTyVars :: InferMode -> [PredType]
+                 -> [(Name,TcType)]
+                 -> TcM (TcTyCoVarSet, [PredType])
+-- Decide which tyvars cannot be generalised:
+--   (a) Free in the environment
+--   (b) Mentioned in a constraint we can't generalise
+--   (c) Connected by an equality to (a) or (b)
+-- Also return the reduced set of constraint we can generalise
+decideMonoTyVars infer_mode candidates name_taus
+  = do { (no_quant, yes_quant) <- pick infer_mode candidates
+
+       ; gbl_tvs <- tcGetGlobalTyCoVars
+       ; let eq_constraints        = filter isEqPred candidates
+             constrained_tvs       = tyCoVarsOfTypes no_quant
+             mono_tvs              = growThetaTyVars eq_constraints $
+                                     gbl_tvs `unionVarSet` constrained_tvs
+
+           -- Warn about the monomorphism restriction
+       ; warn_mono <- woptM Opt_WarnMonomorphism
+       ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
+         do { taus <- mapM (TcM.zonkTcType . snd) name_taus
+            ; warnTc (Reason Opt_WarnMonomorphism)
+                     (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+                     mr_msg }
+
+       ; return (mono_tvs, yes_quant) }
+  where
+    pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
+    -- Split the candidates into ones we definitely
+    -- won't quantify, and ones that we might
+    pick NoRestrictions  cand = return ([], cand)
+    pick ApplyMR         cand = return (cand, [])
+    pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
+                                   ; return (partition (is_int_ct os) cand) }
+
+    is_int_ct ovl_strings pred
+      | Just (cls, _) <- getClassPredTys_maybe pred
+      = isInteractiveClass ovl_strings cls
+      | otherwise
+      = False
+
+    pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
+    mr_msg = hang (text "The Monomorphism Restriction applies to the binding"
+                   <> plural name_taus <+> text "for" <+> pp_bndrs)
+                2 (text "Consider giving a type signature for"
+                   <+> if isSingleton name_taus then pp_bndrs
+                                                else text "these binders")
+
+-------------------
+defaultTyVarsAndSimplify :: TcLevel
+                         -> TyCoVarSet
+                         -> [PredType]          -- Assumed zonked
+                         -> TcM [PredType]      -- Guaranteed Zonked
+-- Default any tyvar free in the constraints,
+-- and re-simplify in case the defaulting allows futher simplification
+defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+  | null candidates  -- Common shortcut
+  = return []
+  | otherwise
+  = do { let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+                = candidateQTyVarsOfTypes candidates
+       ; poly_kinds  <- xoptM LangExt.PolyKinds
+       ; default_kvs <- mapM (default_one poly_kinds True)
+                             (dVarSetElems cand_kvs)
+       ; default_tvs <- mapM (default_one poly_kinds False)
+                             (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+       ; if (not (or default_kvs || or default_tvs))
+         then return candidates
+         else do { candidates' <- simplify_cand candidates
+                 ; traceTc "Simplified after defaulting" $
+                      vcat [ text "Before:" <+> ppr candidates
+                           , text "After:"  <+> ppr candidates' ]
+                 ; return candidates' } }
+  where
+    default_one poly_kinds is_kind_var tv
+      | not (isMetaTyVar tv)
+      = return False
+      | tv `elemVarSet` mono_tvs
+      = return False
+      | otherwise
+      = defaultTyVar (not poly_kinds && is_kind_var) tv
+
+    simplify_cand candidates
+      = do { clone_wanteds <- newWanteds DefaultOrigin candidates
+           ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
+                                           simplifyWantedsTcM clone_wanteds
+              -- Discard evidence; simples is fully zonked
+
+           ; traceTc "Minimise theta" (ppr candidates $$ ppr simples)
+           ; return (ctsPreds simples) }
+
+------------------
+decideQuantifiedTyVars
+   :: TyCoVarSet
+   -> [PredType]   -- Candidates predicates (zonked)
+   -> [PredType] -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
+   -> TcM [TyVar]
+-- Fix what tyvars we are going to quantify over, and quantify them
+decideQuantifiedTyVars mono_tvs candidates psig_theta name_taus
+  = do { zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ map snd name_taus)
+         -- Why psig_theta? see Note [Quantification and partial signatures]
 
        ; let -- The candidate tyvars are the ones free in
              -- either quant_cand or zonked_taus.
              DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
-                = candidateQTyVarsOfTypes (quant_cand ++ zonked_taus)
+                = candidateQTyVarsOfTypes (candidates ++ zonked_taus)
 
-               -- Now keep only the ones reachable
-               -- (via growThetaTyVars) from zonked_taus.
-             grown_tvs = growThetaTyVars quant_cand (tyCoVarsOfTypes zonked_taus)
+             -- Now keep only the ones reachable
+             -- (via growThetaTyVars) from zonked_taus.
+             tau_tvs   = tyCoVarsOfTypes zonked_taus
+             grown_tvs = growThetaTyVars candidates tau_tvs
              pick      = filterDVarSet (`elemVarSet` grown_tvs)
              dvs_plus  = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
 
-       ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
+       ; quantifyZonkedTyVars mono_tvs dvs_plus
           -- We don't grow the kvs, as there's no real need to. Recall
           -- that quantifyTyVars uses the separation between kvs and tvs
           -- only for defaulting, and we don't want (ever) to default a tv
           -- to *. So, don't grow the kvs.
-
-       ; quant_cand <- TcM.zonkTcTypes quant_cand
-                 -- quantifyTyVars turned some meta tyvars into
-                 -- quantified skolems, so we have to zonk again
-
-       ; let qtv_set   = mkVarSet qtvs
-             theta     = pickQuantifiablePreds qtv_set quant_cand
-             min_theta = mkMinimalBySCs theta
-               -- See Note [Minimize by Superclasses]
-
-           -- Warn about the monomorphism restriction
-       ; warn_mono <- woptM Opt_WarnMonomorphism
-       ; let mr_bites | ApplyMR <- infer_mode
-                      = constrained_tvs `intersectsVarSet` grown_tvs
-                      | otherwise
-                      = False
-       ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
-         hang (text "The Monomorphism Restriction applies to the binding"
-               <> plural bndrs <+> text "for" <+> pp_bndrs)
-             2 (text "Consider giving a type signature for"
-                <+> if isSingleton bndrs then pp_bndrs
-                                         else text "these binders")
-
-       ; traceTc "decideQuantification"
-           (vcat [ text "infer_mode:"   <+> ppr infer_mode
-                 , text "gbl_cand:"     <+> ppr gbl_cand
-                 , text "quant_cand:"   <+> ppr quant_cand
-                 , text "zonked_taus:" <+> ppr zonked_taus
-                 , text "gbl_tvs:"      <+> ppr gbl_tvs
-                 , text "mono_tvs:"     <+> ppr mono_tvs
-                 , text "cand_tvs"      <+> ppr cand_tvs
-                 , text "grown_tvs:"    <+> ppr grown_tvs
-                 , text "qtvs:"         <+> ppr qtvs
-                 , text "min_theta:"    <+> ppr min_theta ])
-       ; return (qtvs, min_theta) }
-  where
-    pp_bndrs = pprWithCommas (quotes . ppr) bndrs
-    (bndrs, taus) = unzip name_taus
+       }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
@@ -1603,17 +1672,6 @@ promoteTyVarTcS tclvl tv
   | otherwise
   = return ()
 
--- | If the tyvar is a RuntimeRep var, set it to LiftedRep.
-defaultTyVar :: TcTyVar -> TcM ()
--- Precondition: MetaTyVars only
--- See Note [DefaultTyVar]
-defaultTyVar the_tv
-  | isRuntimeRepVar the_tv
-  = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
-       ; writeMetaTyVar the_tv liftedRepTy }
-
-  | otherwise = return ()    -- The common case
-
 -- | Like 'defaultTyVar', but in the TcS monad.
 defaultTyVarTcS :: TcTyVar -> TcS Bool
 defaultTyVarTcS the_tv
index 0a1b9d3..5bc6aca 100644 (file)
@@ -1,18 +1,16 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[[a]]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: [a] (bound at ExtraTcsUntch.hs:21:3)
-        f :: [a] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: p (bound at ExtraTcsUntch.hs:21:3)
+        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[[a]]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’
+      The type variable ‘a0’ is ambiguous
     • In the first argument of ‘h’, namely ‘[[undefined]]’
       In the expression: h [[undefined]]
       In the expression: (h [[undefined]], op x [y])
-    • Relevant bindings include
-        x :: [a] (bound at ExtraTcsUntch.hs:21:3)
-        f :: [a] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
diff --git a/testsuite/tests/typecheck/should_compile/T13509.hs b/testsuite/tests/typecheck/should_compile/T13509.hs
new file mode 100644 (file)
index 0000000..b910dd5
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE UnboxedTuples, MagicHash #-}
+module T13509 where
+
+import GHC.Exts
+import Data.Word
+
+selectPower :: Word# -> (# Word#, Word# #)
+selectPower base = go base
+  where
+--    go :: Word# -> (# Word#, Word# #)
+    go pw = case timesWord2# pw pw of
+        (# 0##, pw2 #)
+          -> let (# n, pw2n #) = go pw2 in
+            case timesWord2# pw pw2n of
+              (# 0##, pw2n1 #) -> (#n `timesWord#` 2## `plusWord#` 1##, pw2n1 #)
+              _ -> (# n `timesWord#` 2##, pw2n #)
+        _           -> (# 1##, pw #)
index 2436a71..bbf3ccd 100644 (file)
@@ -552,3 +552,5 @@ test('T13458', normal, compile, [''])
 test('T13490', normal, compile, [''])
 test('T13474', normal, compile, [''])
 test('T13524', expect_broken(13524), compile, [''])
+test('T13509', normal, compile, [''])
+