+section: compiler

+issues: #27844

+mrs: !16723

+synopsis:

+  Reinstate a missing occurs check in the constraint solver

+description:

+  Simplifies code in GHC's type-constraint solver, thereby fixing an outright

+  compiler loop (via a missing occurs check).

+

+unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification).

+import GHC.Tc.Types( TcM )

+import GHC.Types.Var

+import GHC.Data.Bag

+

+  = Stage $ do { traceTcS "canonicaliseEquality {" $

+               ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2

+               ; traceTcS "canonicaliseEquality }" (ppr res)

+               ; return res }

+For g we get [G] g1 : UnF (F a) ~ a

+            SUC_CannotUnify -> finish_no_unify

+            SUC_CanUnify    -> do_unification lhs_tv (mkReflRedn Nominal rhs)

+            SUC_NotSure     ->

+              --

+              -- Next, do a fully `checkTyEqRhs` check to see if we can unify

+              -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify

+                  ; traceTcS "canEqCanLHSFinish_try_unification" $

+                    vcat [ text "lhs" <+> ppr lhs

+                         , text "rhs" <+> ppr rhs

+                         , text "check_result" <+> ppr check_result ]

+                      PuFail {}         -> finish_no_unify

+                      PuOK cts rhs_redn -> do { emitWork cts

+                                              ; do_unification lhs_tv rhs_redn } }

+    -- finish_no_unify: abandon the attempt to unify, and instead hand off to

+    -- canEqCanLHSFinish_no_unification

+    -- First, though, if we have (tv ~ F tys)

+    --        swap it over so we get (F tys ~ tv), with `F tys` on the LHS

+    -- See Note [Orienting TyVarLHS/TyFamLHS]

+    finish_no_unify

+      | TyVarLHS lhs_tv <- lhs

+      , Just can_rhs <- canTyFamEqLHS_maybe rhs

+      = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv)

+      | otherwise

+      = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs

+

+    -- do_unification: Phew! Finally!  We can unify; go ahead and do so.

+    do_unification tv rhs_redn =

+                              -- emptyCoHoleSet: we are about to /solve/ this

+                              -- constraint, so its CoHoleSet doesn't matter

+  -- We can't unify, but we can see if this equality can go in the inert set

+  -- and be used to rewrite other constraints.

+  -- See Note [Equalities where unification fails]

+  = do { -- Do checkTypeEqNoUnfication to guarantee (TyEq:OC), (TyEq:F)

+       ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs

+              -> -- We can't unify, and this equality should not be used to rewrite

+                 -- other constraints (e.g. because it has an occurs check).

+                 -- So add it to the inert Irreds.

+                 do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs

+                    ; finishCanWithIrred (NonCanonicalReason reason) new_ev }

+              -> -- Put this constraint into the inert set, so that it will be used

+                 -- to solve or rewrite other constraints.

+                 --

+                 -- NB: checkTypeEqNoUnification does not check for

+                 --     (b) skolem-escape (tefTyVar_levelCheck = LC_None)

+                 --     (a) concreteness  (tefTyVar_concreteCheck = CC_None)

+                 --   So an equality whose only problem is e.g. skolem-escape will

+                 --   return PuOK, will be put in the inert set, will be used for

+                 --   rewriting. That is fine.

+                 --

+                 -- assertPpr (isEmptyCts new_eqs):

+                 --   checkTypeEqNoUnification does neither promotion nor type-family

+                 --   flattening for Wanteds, and hence creates no equalities to solve

+                 assertPpr (isEmptyCts new_eqs)

+                    (vcat [ text "new_eqs"  <+> ppr new_eqs

+                          , text "rhs_redn" <+> ppr rhs_redn

+                          , text "lhs"      <+> ppr lhs

+                          , text "rhs"      <+> ppr rhs ]) $

+                 do { let lhs_ty    = canEqLHSType lhs

+                    ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet

+checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType

+                         -> TcS (PuResult Ct Reduction)

+-- Used for general CanEqLHSs, when we have decided that we cannot unify

+checkTypeEqNoUnification ev eq_rel lhs rhs =

+  case ev of

+    CtGiven {} ->

+      do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs

+                                                  , text "rhs:" <+> ppr rhs ])

+         ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)

+         ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)

+         ; case check_result of

+              PuFail reason -> return (PuFail reason)

+              PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs

+                                  ; emitWork new_givens

+                                  ; updInertSet (addCycleBreakerBindings prs)

+                                  ; return (pure redn) } }

+    CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $

+                        vcat [ text "lhs:" <+> ppr lhs

+                             , text "rhs:" <+> ppr rhs ]

+                      ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)

+                      ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)

+                      ; return check_result }

+  where

+    wanted_flags :: TyEqFlags TcM Ct

+    wanted_flags = notUnifying_TEFTask occ_prob lhs

+        -- See Note [Don't cycle-break Wanteds when not unifying]

+

+    given_flags :: TyEqFlags TcM (TcTyVar, TcType)

+    given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }

+        -- TEFA_Break used for: [G] a ~ Maybe (F a)

+        --                   or [G] F a ~ Maybe (F a)

+

+    -- occ_prob: see Note [Occurs check and representational equality]

+    occ_prob = case eq_rel of

+                 NomEq  -> cteInsolubleOccurs

+                 ReprEq -> cteSolubleOccurs

+

+    ---------------------------

+    mk_new_given :: (TcTyVar, TcType) -> TcS Ct

+    mk_new_given (new_tv, fam_app)

+      = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)

+      where

+        new_ty     = mkTyVarTy new_tv

+        given_pred = mkNomEqPred fam_app new_ty

+        given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note

+    -- See Detail (7) of the Note

+    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin

+{- Note [Equalities where unification fails]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+If we can't unify, but the equality is canonical, we still want to add it to the

+inert set so that it can be used to rewrite other Wanteds.  (There are many

+reasons by unification might not happen: the LHS is not a touchable unification

+variable, it has rewriters, it's a Given etc.)

+

+* In this case we call `checkTypeEqNoUnification`to see if it is canonical (which

+  in turn calls `checkTypeEqRhs` with suitable flags).

+

+* NB: we do /not/ try to take advantage of the case where

+  `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so

+  caused #27844.  (The first call did fam-app breaking, which concealed a genuine

+  occurs check.)  It's just too clever; better to do the simple thing.

+

+Note [Don't cycle-break Wanteds when not unifying]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+Consdier

+  [W] a[2] ~ Maybe (F a[2])

+

+Should we cycle-break this Wanted, thus?

+

+  [W] a[2] ~ Maybe delta[2]

+  [W] delta[2] ~ F a[2]

+

+For a start, this is dodgy because we might just unify delta, thus undoing

+what we have done, and getting an infinite loop in the solver.  Even if we

+somehow prevented ourselves from doing so, is there any merit in the split?

+Maybe: perhaps we can use that equality on `a` to unlock other constraints?

+Consider

+  type instance F (Maybe _) = Bool

+

+  [G] g1: a ~ Maybe Bool

+  [W] w1: a ~ Maybe (F a)

+

+If we loop-break w1 to get

+  [W] w1': a ~ Maybe gamma

+  [W] w3:  gamma ~ F a

+Now rewrite w3 with w1'

+  [W] w3':  gamma ~ F (Maybe gamma)

+Now use the type instance to get

+  gamma := Bool

+Now we are left with

+  [W] w1': a ~ Maybe Bool

+which we can solve from the Given.

+

+BUT in this situation we could have rewritten the

+/original/ Wanted from the Given, like this:

+  [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))

+and that is readily soluble.

+

+In short: loop-breaking Wanteds, when we aren't unifying,

+seems of no merit.  Hence TEFA_Recurse, rather than TEFA_Break,

+in `wanted_flags` in `checkTypeEqNoUnification`.

+

+Note [Equalities with heterogeneous kinds]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+to our new cbv. This is actually done by `break_given` in `checkTypeEqNoUnification`.

+    This is done during canonicalisation, in checkTyEqRhs; invariant

+    pprEq

+-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'.

+-- (use the full 'checkTyEqRhs').

+-- It returns SUC_CannotUnify for

+--   * Touchability failure

+--   * Top level-shape failure

+--

+-- It returns SUC_NotSure for

+--   * Occurs check: lhs_tv occurs in rhs_ty

+--   * Type families unless fam_ok=True

+--   * Foralls unless

+--        lhs_tv is RuntimeUnk (used by GHCi debugger)

+--            or is a QL instantiation variable

+--   * Concreteness: lhs_tv is concrete and rhs is a non-concrete type

+--   * Skolem-escape: a level-check for type variables, to avoid skolem escape

+and checks to see if `rhs` satisfies, /or can be made to satisfy/,

+Note "or can be made to satisfy the preconditions"!  `checkTyEqRhs` may transform

+the RHS by

+

+  * Turning a type-family application into a type variable, perhaps to avoid

+    an occurs check.  See Note Note [Family applications in canonical constraints]

+

+  * Promoting any nested unification variables, in order to satisfy the

+    level invariant. See Note [Promotion and level-checking]

+

+in canEqCanLHS2, before getting to checkTyEqRhs.

+    • Couldn't match type ‘m’ with ‘Int’

+      ‘m’ is a rigid type variable bound by

+{-# OPTIONS_GHC -ddump-simpl #-}

+

+-- #7803: foo1 should be fully specialised at Double.  In the bug report

+-- it ended up calling the overloaded exp5Tail (with a dictionary argument),

+-- because the specialiser ran before the overloaded call was floated to

+-- the top level.  So the dumped Core for this module must mention no

+-- exp5Tail at all.

+module T7803 (foo1) where

+

+import T7803a

+

+bar :: Floating a => a -> a -> a

+bar z = subtract (evaluate integ z) . evaluate integ

+  where

+    integ = indefinite (Piecewise [Poly4 1])

+{-# SPECIALIZE bar :: Double -> Double -> Double #-}

+

+foo :: Floating a => a -> a -> a

+foo x = bar x

+{-# SPECIALIZE foo :: Double -> Double -> Double #-}

+

+foo1 :: Double -> Double -> Double

+foo1 x = foo x

+foo1

+{-# LANGUAGE ConstraintKinds #-}

+{-# LANGUAGE FlexibleContexts #-}

+{-# LANGUAGE FlexibleInstances #-}

+{-# LANGUAGE MultiParamTypeClasses #-}

+{-# LANGUAGE TypeFamilies #-}

+{-# LANGUAGE UndecidableInstances #-}

+{-# LANGUAGE UndecidableSuperClasses #-}

+

+module T7803a

+    ( Evaluate (..)

+    , HasIntegral (..)

+    , Poly4 (..)

+    , Domain

+    , IntOfLogPoly4 (..)

+    , Piecewise (..)

+    ) where

+

+import Data.Kind (Constraint, Type)

+

+class Evaluate poly where

+    evaluate :: (Domain' poly a) => poly a -> a -> a

+

+class Evaluate (IntegralOf poly) => HasIntegral poly where

+    type IntegralOf poly :: Type -> Type

+    indefinite :: (Domain' poly a, Domain' (IntegralOf poly) a)

+               => poly a -> IntegralOf poly a

+

+type family Domain (f :: Type -> Type) a :: Constraint

+

+class Domain f a => Domain' f a

+instance Domain f a => Domain' f a

+

+newtype Poly4 a = Poly4 { poly4_a :: a }

+

+type instance Domain Poly4 a = Fractional a

+

+data IntOfLogPoly4 a = IntOfLogPoly4 { ilp4_k :: !a, ilp4_u :: !a }

+

+type instance Domain IntOfLogPoly4 a = Floating a

+

+instance Evaluate IntOfLogPoly4 where

+    evaluate (IntOfLogPoly4 k _) x = k + x * exp5Tail (- log x)

+    {-# INLINE evaluate #-}

+

+{-# RULES "exp5Tail/Double" exp5Tail = exp5TailDouble #-}

+{-# NOINLINE exp5Tail #-}

+

+exp5Tail :: (Floating a) => a -> a

+exp5Tail x = x / 120

+

+exp5TailDouble :: Double -> Double

+exp5TailDouble x = x / 120

+

+instance HasIntegral Poly4 where

+    type IntegralOf Poly4 = IntOfLogPoly4

+    indefinite = \ (Poly4 a) -> IntOfLogPoly4 0 a

+    {-# INLINE indefinite #-}

+

+newtype Piecewise poly a = Piecewise { unPiecewise :: [poly a] }

+

+type instance Domain (Piecewise poly) a = (Domain poly a, Num a)

+

+instance (Evaluate poly) => Evaluate (Piecewise poly) where

+    evaluate = \ (Piecewise pp) x ->

+        case pp of

+          p : _ -> evaluate p x

+          []    -> error "evaluate: empty Piecewise"

+    {-# INLINE evaluate #-}

+

+instance (HasIntegral poly) => HasIntegral (Piecewise poly) where

+    type IntegralOf (Piecewise poly) = Piecewise (IntegralOf poly)

+    indefinite (Piecewise m) = Piecewise $ map indefinite m

+    {-# INLINE indefinite #-}

+# T7803: we expect NO calls to the overloaded 'exp5Tail' in T7803.hs

+# In the bug report #7803, the unspecialised call was signalled by 'exp5Tail'

+#    in foo1's Core, so we grep for that; also for 'foo1', lest we dump nothing

+# One module, T7803.hs, has OPTIONS_GHC -ddump-simpl

+test('T7803', [ grep_errmsg(r'exp5Tail|foo1') ],

+     multimod_compile, ['T7803', '-O2 -v0 -dsuppress-all -dsuppress-uniques -dno-typeable-binds'])

+

+-- Repro.hs

+-- The call to f forces c ~ (b, F c) inside the scope of the skolem b.

+-- Correct behaviour: a type error at the first argument of const

+-- (as GHC 9.12.4 reports).

+

+{-# LANGUAGE RankNTypes, TypeFamilies #-}

+module T27844 where

+

+type family F a

+

+f :: (forall b. b -> (b, F c)) -> c -> ()

+f _ _ = ()

+

+g x = f (\_ -> const x (show x)) x

+T27844.hs:13:22: error: [GHC-25897]

+    • Couldn't match expected type ‘(b, F c)’ with actual type ‘c’

+      ‘c’ is a rigid type variable bound by

+        the inferred type of g :: Show c => c -> ()

+        at T27844.hs:143:1-34

+    • In the first argument of ‘const’, namely ‘x’

+      In the expression: const x (show x)

+      In the first argument of ‘f’, namely ‘(\ _ -> const x (show x))’

+    • Relevant bindings include

+        x :: c (bound at T27844.hs:14:3)

+        g :: c -> () (bound at T27844.hs:14:1)

+test('T27844', normal, compile_fail, [''])