never executed always true always false
    1 {-# LANGUAGE TypeFamilies #-}
    2 
    3 {-
    4 (c) The University of Glasgow 2006
    5 (c) The AQUA Project, Glasgow University, 1993-1998
    6 
    7 -}
    8 
    9 -- | Typechecking rewrite rules
   10 module GHC.Tc.Gen.Rule ( tcRules ) where
   11 
   12 import GHC.Prelude
   13 
   14 import GHC.Hs
   15 import GHC.Tc.Types
   16 import GHC.Tc.Utils.Monad
   17 import GHC.Tc.Solver
   18 import GHC.Tc.Types.Constraint
   19 import GHC.Core.Predicate
   20 import GHC.Tc.Types.Origin
   21 import GHC.Tc.Utils.TcMType
   22 import GHC.Tc.Utils.TcType
   23 import GHC.Tc.Gen.HsType
   24 import GHC.Tc.Gen.Expr
   25 import GHC.Tc.Utils.Env
   26 import GHC.Tc.Utils.Unify( buildImplicationFor )
   27 import GHC.Tc.Types.Evidence( mkTcCoVarCo )
   28 import GHC.Core.Type
   29 import GHC.Core.TyCon( isTypeFamilyTyCon )
   30 import GHC.Types.Id
   31 import GHC.Types.Var( EvVar )
   32 import GHC.Types.Var.Set
   33 import GHC.Types.Basic ( RuleName, allVarsOfKindDefault )
   34 import GHC.Types.SrcLoc
   35 import GHC.Utils.Outputable
   36 import GHC.Utils.Panic
   37 import GHC.Data.FastString
   38 import GHC.Data.Bag
   39 
   40 {-
   41 Note [Typechecking rules]
   42 ~~~~~~~~~~~~~~~~~~~~~~~~~
   43 We *infer* the typ of the LHS, and use that type to *check* the type of
   44 the RHS.  That means that higher-rank rules work reasonably well. Here's
   45 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
   46 
   47    foo :: (forall m. m a -> m b) -> m a -> m b
   48    foo f = ...
   49 
   50    bar :: (forall m. m a -> m a) -> m a -> m a
   51    bar f = ...
   52 
   53    {-# RULES "foo/bar" foo = bar #-}
   54 
   55 He wanted the rule to typecheck.
   56 
   57 Note [TcLevel in type checking rules]
   58 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   59 Bringing type variables into scope naturally bumps the TcLevel. Thus, we type
   60 check the term-level binders in a bumped level, and we must accordingly bump
   61 the level whenever these binders are in scope.
   62 
   63 Note [Re-quantify type variables in rules]
   64 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   65 Consider this example from #17710:
   66 
   67   foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
   68   foo x = Proxy
   69   {-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}
   70 
   71 Written out in more detail, the "foo" rewrite rule looks like this:
   72 
   73   forall k (a :: k). forall (x :: Proxy (a :: k)). foo @k @a @b0 x = Proxy @k @b0
   74 
   75 Where b0 is a unification variable. Where should b0 be quantified? We have to
   76 quantify it after k, since (b0 :: k). But generalization usually puts inferred
   77 type variables (such as b0) at the /front/ of the telescope! This creates a
   78 conflict.
   79 
   80 One option is to simply throw an error, per the principles of
   81 Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType. This is what would happen
   82 if we were generalising over a normal type signature. On the other hand, the
   83 types in a rewrite rule aren't quite "normal", since the notions of specified
   84 and inferred type variables aren't applicable.
   85 
   86 A more permissive design (and the design that GHC uses) is to simply requantify
   87 all of the type variables. That is, we would end up with this:
   88 
   89   forall k (a :: k) (b :: k). forall (x :: Proxy (a :: k)). foo @k @a @b x = Proxy @k @b
   90 
   91 It's a bit strange putting the generalized variable `b` after the user-written
   92 variables `k` and `a`. But again, the notion of specificity is not relevant to
   93 rewrite rules, since one cannot "visibly apply" a rewrite rule. This design not
   94 only makes "foo" typecheck, but it also makes the implementation simpler.
   95 
   96 See also Note [Generalising in tcTyFamInstEqnGuts] in GHC.Tc.TyCl, which
   97 explains a very similar design when generalising over a type family instance
   98 equation.
   99 -}
  100 
  101 tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTc]
  102 tcRules decls = mapM (wrapLocMA tcRuleDecls) decls
  103 
  104 tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
  105 tcRuleDecls (HsRules { rds_src = src
  106                      , rds_rules = decls })
  107    = do { tc_decls <- mapM (wrapLocMA tcRule) decls
  108         ; return $ HsRules { rds_ext   = noExtField
  109                            , rds_src   = src
  110                            , rds_rules = tc_decls } }
  111 
  112 tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
  113 tcRule (HsRule { rd_ext  = ext
  114                , rd_name = rname@(L _ (_,name))
  115                , rd_act  = act
  116                , rd_tyvs = ty_bndrs
  117                , rd_tmvs = tm_bndrs
  118                , rd_lhs  = lhs
  119                , rd_rhs  = rhs })
  120   = addErrCtxt (ruleCtxt name)  $
  121     do { traceTc "---- Rule ------" (pprFullRuleName rname)
  122 
  123         -- Note [Typechecking rules]
  124        ; (tc_lvl, stuff) <- pushTcLevelM $
  125                             generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
  126 
  127        ; let (id_bndrs, lhs', lhs_wanted
  128                       , rhs', rhs_wanted, rule_ty) = stuff
  129 
  130        ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname
  131                                   , ppr lhs_wanted
  132                                   , ppr rhs_wanted ])
  133 
  134        ; (lhs_evs, residual_lhs_wanted)
  135             <- simplifyRule name tc_lvl lhs_wanted rhs_wanted
  136 
  137        -- SimplfyRule Plan, step 4
  138        -- Now figure out what to quantify over
  139        -- c.f. GHC.Tc.Solver.simplifyInfer
  140        -- We quantify over any tyvars free in *either* the rule
  141        --  *or* the bound variables.  The latter is important.  Consider
  142        --      ss (x,(y,z)) = (x,z)
  143        --      RULE:  forall v. fst (ss v) = fst v
  144        -- The type of the rhs of the rule is just a, but v::(a,(b,c))
  145        --
  146        -- We also need to get the completely-unconstrained tyvars of
  147        -- the LHS, lest they otherwise get defaulted to Any; but we do that
  148        -- during zonking (see GHC.Tc.Utils.Zonk.zonkRule)
  149 
  150        ; let tpl_ids = lhs_evs ++ id_bndrs
  151 
  152        -- See Note [Re-quantify type variables in rules]
  153        ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
  154        ; qtkvs <- quantifyTyVars allVarsOfKindDefault forall_tkvs
  155        ; traceTc "tcRule" (vcat [ pprFullRuleName rname
  156                                 , ppr forall_tkvs
  157                                 , ppr qtkvs
  158                                 , ppr rule_ty
  159                                 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
  160                   ])
  161 
  162        -- SimplfyRule Plan, step 5
  163        -- Simplify the LHS and RHS constraints:
  164        -- For the LHS constraints we must solve the remaining constraints
  165        -- (a) so that we report insoluble ones
  166        -- (b) so that we bind any soluble ones
  167        ; let skol_info = RuleSkol name
  168        ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
  169                                          lhs_evs residual_lhs_wanted
  170        ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
  171                                          lhs_evs rhs_wanted
  172 
  173        ; emitImplications (lhs_implic `unionBags` rhs_implic)
  174        ; return $ HsRule { rd_ext = ext
  175                          , rd_name = rname
  176                          , rd_act = act
  177                          , rd_tyvs = ty_bndrs -- preserved for ppr-ing
  178                          , rd_tmvs = map (noLocA . RuleBndr noAnn . noLocA)
  179                                          (qtkvs ++ tpl_ids)
  180                          , rd_lhs  = mkHsDictLet lhs_binds lhs'
  181                          , rd_rhs  = mkHsDictLet rhs_binds rhs' } }
  182 
  183 generateRuleConstraints :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
  184                         -> LHsExpr GhcRn -> LHsExpr GhcRn
  185                         -> TcM ( [TcId]
  186                                , LHsExpr GhcTc, WantedConstraints
  187                                , LHsExpr GhcTc, WantedConstraints
  188                                , TcType )
  189 generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
  190   = do { ((tv_bndrs, id_bndrs), bndr_wanted) <- captureConstraints $
  191                                                 tcRuleBndrs ty_bndrs tm_bndrs
  192               -- bndr_wanted constraints can include wildcard hole
  193               -- constraints, which we should not forget about.
  194               -- It may mention the skolem type variables bound by
  195               -- the RULE.  c.f. #10072
  196 
  197        ; tcExtendTyVarEnv tv_bndrs $
  198          tcExtendIdEnv    id_bndrs $
  199     do { -- See Note [Solve order for RULES]
  200          ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
  201        ; (rhs',            rhs_wanted) <- captureConstraints $
  202                                           tcCheckMonoExpr rhs rule_ty
  203        ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
  204        ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
  205 
  206 -- See Note [TcLevel in type checking rules]
  207 tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
  208             -> TcM ([TcTyVar], [Id])
  209 tcRuleBndrs (Just bndrs) xs
  210   = do { (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol bndrs $
  211                                   tcRuleTmBndrs xs
  212        ; let tys1 = binderVars tybndrs1
  213        ; return (tys1 ++ tys2, tms) }
  214 
  215 tcRuleBndrs Nothing xs
  216   = tcRuleTmBndrs xs
  217 
  218 -- See Note [TcLevel in type checking rules]
  219 tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
  220 tcRuleTmBndrs [] = return ([],[])
  221 tcRuleTmBndrs (L _ (RuleBndr _ (L _ name)) : rule_bndrs)
  222   = do  { ty <- newOpenFlexiTyVarTy
  223         ; (tyvars, tmvars) <- tcRuleTmBndrs rule_bndrs
  224         ; return (tyvars, mkLocalId name Many ty : tmvars) }
  225 tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
  226 --  e.g         x :: a->a
  227 --  The tyvar 'a' is brought into scope first, just as if you'd written
  228 --              a::*, x :: a->a
  229 --  If there's an explicit forall, the renamer would have already reported an
  230 --   error for each out-of-scope type variable used
  231   = do  { let ctxt = RuleSigCtxt name
  232         ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
  233         ; let id  = mkLocalId name Many id_ty
  234                     -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
  235 
  236               -- The type variables scope over subsequent bindings; yuk
  237         ; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
  238                                    tcRuleTmBndrs rule_bndrs
  239         ; return (map snd tvs ++ tyvars, id : tmvars) }
  240 
  241 ruleCtxt :: FastString -> SDoc
  242 ruleCtxt name = text "When checking the rewrite rule" <+>
  243                 doubleQuotes (ftext name)
  244 
  245 
  246 {-
  247 *********************************************************************************
  248 *                                                                                 *
  249               Constraint simplification for rules
  250 *                                                                                 *
  251 ***********************************************************************************
  252 
  253 Note [The SimplifyRule Plan]
  254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  255 Example.  Consider the following left-hand side of a rule
  256         f (x == y) (y > z) = ...
  257 If we typecheck this expression we get constraints
  258         d1 :: Ord a, d2 :: Eq a
  259 We do NOT want to "simplify" to the LHS
  260         forall x::a, y::a, z::a, d1::Ord a.
  261           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
  262 Instead we want
  263         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
  264           f ((==) d2 x y) ((>) d1 y z) = ...
  265 
  266 Here is another example:
  267         fromIntegral :: (Integral a, Num b) => a -> b
  268         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
  269 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
  270 we *dont* want to get
  271         forall dIntegralInt.
  272            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
  273 because the scsel will mess up RULE matching.  Instead we want
  274         forall dIntegralInt, dNumInt.
  275           fromIntegral Int Int dIntegralInt dNumInt = id Int
  276 
  277 Even if we have
  278         g (x == y) (y == z) = ..
  279 where the two dictionaries are *identical*, we do NOT WANT
  280         forall x::a, y::a, z::a, d1::Eq a
  281           f ((==) d1 x y) ((>) d1 y z) = ...
  282 because that will only match if the dict args are (visibly) equal.
  283 Instead we want to quantify over the dictionaries separately.
  284 
  285 In short, simplifyRuleLhs must *only* squash equalities, leaving
  286 all dicts unchanged, with absolutely no sharing.
  287 
  288 Also note that we can't solve the LHS constraints in isolation:
  289 Example   foo :: Ord a => a -> a
  290           foo_spec :: Int -> Int
  291           {-# RULE "foo"  foo = foo_spec #-}
  292 Here, it's the RHS that fixes the type variable
  293 
  294 HOWEVER, under a nested implication things are different
  295 Consider
  296   f :: (forall a. Eq a => a->a) -> Bool -> ...
  297   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
  298        f b True = ...
  299     #-}
  300 Here we *must* solve the wanted (Eq a) from the given (Eq a)
  301 resulting from skolemising the argument type of g.  So we
  302 revert to SimplCheck when going under an implication.
  303 
  304 
  305 --------- So the SimplifyRule Plan is this -----------------------
  306 
  307 * Step 0: typecheck the LHS and RHS to get constraints from each
  308 
  309 * Step 1: Simplify the LHS and RHS constraints all together in one bag
  310           We do this to discover all unification equalities
  311 
  312 * Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
  313           advantage of those unifications
  314 
  315 * Setp 3: Partition the LHS constraints into the ones we will
  316           quantify over, and the others.
  317           See Note [RULE quantification over equalities]
  318 
  319 * Step 4: Decide on the type variables to quantify over
  320 
  321 * Step 5: Simplify the LHS and RHS constraints separately, using the
  322           quantified constraints as givens
  323 
  324 Note [Solve order for RULES]
  325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  326 In step 1 above, we need to be a bit careful about solve order.
  327 Consider
  328    f :: Int -> T Int
  329    type instance T Int = Bool
  330 
  331    RULE f 3 = True
  332 
  333 From the RULE we get
  334    lhs-constraints:  T Int ~ alpha
  335    rhs-constraints:  Bool ~ alpha
  336 where 'alpha' is the type that connects the two.  If we glom them
  337 all together, and solve the RHS constraint first, we might solve
  338 with alpha := Bool.  But then we'd end up with a RULE like
  339 
  340     RULE: f 3 |> (co :: T Int ~ Bool) = True
  341 
  342 which is terrible.  We want
  343 
  344     RULE: f 3 = True |> (sym co :: Bool ~ T Int)
  345 
  346 So we are careful to solve the LHS constraints first, and *then* the
  347 RHS constraints.  Actually much of this is done by the on-the-fly
  348 constraint solving, so the same order must be observed in
  349 tcRule.
  350 
  351 
  352 Note [RULE quantification over equalities]
  353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  354 Deciding which equalities to quantify over is tricky:
  355  * We do not want to quantify over insoluble equalities (Int ~ Bool)
  356     (a) because we prefer to report a LHS type error
  357     (b) because if such things end up in 'givens' we get a bogus
  358         "inaccessible code" error
  359 
  360  * But we do want to quantify over things like (a ~ F b), where
  361    F is a type function.
  362 
  363 The difficulty is that it's hard to tell what is insoluble!
  364 So we see whether the simplification step yielded any type errors,
  365 and if so refrain from quantifying over *any* equalities.
  366 
  367 Note [Quantifying over coercion holes]
  368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  369 Equality constraints from the LHS will emit coercion hole Wanteds.
  370 These don't have a name, so we can't quantify over them directly.
  371 Instead, because we really do want to quantify here, invent a new
  372 EvVar for the coercion, fill the hole with the invented EvVar, and
  373 then quantify over the EvVar. Not too tricky -- just some
  374 impedance matching, really.
  375 
  376 Note [Simplify cloned constraints]
  377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  378 At this stage, we're simplifying constraints only for insolubility
  379 and for unification. Note that all the evidence is quickly discarded.
  380 We use a clone of the real constraint. If we don't do this,
  381 then RHS coercion-hole constraints get filled in, only to get filled
  382 in *again* when solving the implications emitted from tcRule. That's
  383 terrible, so we avoid the problem by cloning the constraints.
  384 
  385 -}
  386 
  387 simplifyRule :: RuleName
  388              -> TcLevel                 -- Level at which to solve the constraints
  389              -> WantedConstraints       -- Constraints from LHS
  390              -> WantedConstraints       -- Constraints from RHS
  391              -> TcM ( [EvVar]               -- Quantify over these LHS vars
  392                     , WantedConstraints)    -- Residual un-quantified LHS constraints
  393 -- See Note [The SimplifyRule Plan]
  394 -- NB: This consumes all simple constraints on the LHS, but not
  395 -- any LHS implication constraints.
  396 simplifyRule name tc_lvl lhs_wanted rhs_wanted
  397   = do {
  398        -- Note [The SimplifyRule Plan] step 1
  399        -- First solve the LHS and *then* solve the RHS
  400        -- Crucially, this performs unifications
  401        -- Why clone?  See Note [Simplify cloned constraints]
  402        ; lhs_clone <- cloneWC lhs_wanted
  403        ; rhs_clone <- cloneWC rhs_wanted
  404        ; setTcLevel tc_lvl $
  405          runTcSDeriveds    $
  406          do { _ <- solveWanteds lhs_clone
  407             ; _ <- solveWanteds rhs_clone
  408                   -- Why do them separately?
  409                   -- See Note [Solve order for RULES]
  410             ; return () }
  411 
  412        -- Note [The SimplifyRule Plan] step 2
  413        ; lhs_wanted <- zonkWC lhs_wanted
  414        ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
  415 
  416        -- Note [The SimplifyRule Plan] step 3
  417        ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
  418 
  419        ; traceTc "simplifyRule" $
  420          vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
  421               , text "lhs_wanted" <+> ppr lhs_wanted
  422               , text "rhs_wanted" <+> ppr rhs_wanted
  423               , text "quant_cts" <+> ppr quant_cts
  424               , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
  425               ]
  426 
  427        ; return (quant_evs, residual_lhs_wanted) }
  428 
  429   where
  430     mk_quant_ev :: Ct -> TcM EvVar
  431     mk_quant_ev ct
  432       | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
  433       = case dest of
  434           EvVarDest ev_id -> return ev_id
  435           HoleDest hole   -> -- See Note [Quantifying over coercion holes]
  436                              do { ev_id <- newEvVar pred
  437                                 ; fillCoercionHole hole (mkTcCoVarCo ev_id)
  438                                 ; return ev_id }
  439     mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
  440 
  441 
  442 getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
  443 -- Extract all the constraints we can quantify over,
  444 --   also returning the depleted WantedConstraints
  445 --
  446 -- NB: we must look inside implications, because with
  447 --     -fdefer-type-errors we generate implications rather eagerly;
  448 --     see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
  449 --
  450 -- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
  451 --   and attempt to solve them from the quantified constraints.  That
  452 --   nearly works, but fails for a constraint like (d :: Eq Int).
  453 --   We /do/ want to quantify over it, but the short-cut solver
  454 --   (see GHC.Tc.Solver.Interact Note [Shortcut solving]) ignores the quantified
  455 --   and instead solves from the top level.
  456 --
  457 --   So we must partition the WantedConstraints ourselves
  458 --   Not hard, but tiresome.
  459 
  460 getRuleQuantCts wc
  461   = float_wc emptyVarSet wc
  462   where
  463     float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
  464     float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
  465       = ( simple_yes `andCts` implic_yes
  466         , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_holes = holes })
  467      where
  468         (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
  469         (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
  470                                                 emptyBag implics
  471 
  472     float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
  473     float_implic skol_tvs yes1 imp
  474       = (yes1 `andCts` yes2, imp { ic_wanted = no })
  475       where
  476         (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
  477         new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
  478 
  479     rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
  480     rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
  481       EqPred _ t1 t2
  482         | not (ok_eq t1 t2)
  483         -> False        -- Note [RULE quantification over equalities]
  484       SpecialPred {}
  485         -- RULES must never quantify over special predicates, as that
  486         -- would leak internal GHC implementation details to the user.
  487         --
  488         -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}.
  489         -> False
  490       _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
  491 
  492     ok_eq t1 t2
  493        | t1 `tcEqType` t2 = False
  494        | otherwise        = is_fun_app t1 || is_fun_app t2
  495 
  496     is_fun_app ty   -- ty is of form (F tys) where F is a type function
  497       = case tyConAppTyCon_maybe ty of
  498           Just tc -> isTypeFamilyTyCon tc
  499           Nothing -> False