Tidy up handling of coercion variables

* Comments to explain that a CoVar, whose IdInfo is CoVarId,
  is always unlifted (but may be nominal or representational role)

  And TyCoRep.isCoercionType picks out only those unlifted
  types, NOT the lifted versions

* Introduce Var.NcId for non-co-var Ids
  with predicate isNonCoVarId

* Add assertions in CoreSubst that the Id env is only
  used for NcIds

* Fix lurking bug in CSE which extended the
  CoreSubst Id env with a CoVar

* Fix two bugs in Specialise.spec_call, which wrongly treated
  CoVars like NcIds
    - needed a varToCoreExpr in one place
    - needed extendSubst not extendIdSubst in another
  This was the root cause of Trac #11644

Minor refactoring

* Eliminate unused mkDerivedLocalCoVarM, mkUserLocalCoVar
* Small refactor in mkSysLocalOrCoVar

10 files changed, 86 insertions, 47 deletions

diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs
index b273b66256..e55259b007 100644
--- a/compiler/basicTypes/Id.hs
+++ b/compiler/basicTypes/Id.hs
@@ -34,8 +34,7 @@ module Id (
         mkLocalIdOrCoVarWithInfo,
         mkLocalIdWithInfo, mkExportedLocalId, mkExportedVanillaId,
         mkSysLocal, mkSysLocalM, mkSysLocalOrCoVar, mkSysLocalOrCoVarM,
-        mkUserLocal, mkUserLocalCoVar, mkUserLocalOrCoVar,
-        mkDerivedLocalCoVarM,
+        mkUserLocal, mkUserLocalOrCoVar,
         mkTemplateLocals, mkTemplateLocalsNum, mkTemplateLocal,
         mkWorkerId,
 
@@ -302,10 +301,7 @@ mkSysLocal fs uniq ty = ASSERT( not (isCoercionType ty) )
 -- | Like 'mkSysLocal', but checks to see if we have a covar type
 mkSysLocalOrCoVar :: FastString -> Unique -> Type -> Id
 mkSysLocalOrCoVar fs uniq ty
-  | isCoercionType ty = mkLocalCoVar name ty
-  | otherwise         = mkLocalId    name ty
-  where
-    name = mkSystemVarName uniq fs
+  = mkLocalIdOrCoVar (mkSystemVarName uniq fs) ty
 
 mkSysLocalM :: MonadUnique m => FastString -> Type -> m Id
 mkSysLocalM fs ty = getUniqueM >>= (\uniq -> return (mkSysLocal fs uniq ty))
@@ -319,23 +315,11 @@ mkUserLocal :: OccName -> Unique -> Type -> SrcSpan -> Id
 mkUserLocal occ uniq ty loc = ASSERT( not (isCoercionType ty) )
                               mkLocalId (mkInternalName uniq occ loc) ty
 
--- | Like 'mkUserLocal' for covars
-mkUserLocalCoVar :: OccName -> Unique -> Type -> SrcSpan -> Id
-mkUserLocalCoVar occ uniq ty loc
-  = mkLocalCoVar (mkInternalName uniq occ loc) ty
-
 -- | Like 'mkUserLocal', but checks if we have a coercion type
 mkUserLocalOrCoVar :: OccName -> Unique -> Type -> SrcSpan -> Id
 mkUserLocalOrCoVar occ uniq ty loc
   = mkLocalIdOrCoVar (mkInternalName uniq occ loc) ty
 
-mkDerivedLocalCoVarM :: MonadUnique m => (OccName -> OccName) -> Id -> Type -> m Id
-mkDerivedLocalCoVarM deriv_name id ty
-    = ASSERT( isCoercionType ty )
-      do { uniq <- getUniqueM
-         ; let name = mkDerivedInternalName deriv_name uniq (getName id)
-         ; return (mkLocalCoVar name ty) }
-
 {-
 Make some local @Ids@ for a template @CoreExpr@.  These have bogus
 @Uniques@, but that's OK because the templates are supposed to be
diff --git a/compiler/basicTypes/IdInfo.hs b/compiler/basicTypes/IdInfo.hs
index 3bc1da0ef4..fd61a9c6b9 100644
--- a/compiler/basicTypes/IdInfo.hs
+++ b/compiler/basicTypes/IdInfo.hs
@@ -134,7 +134,9 @@ data IdDetails
        --                  implemented with a newtype, so it might be bad
        --                  to be strict on this dictionary
 
-  | CoVarId                    -- ^ A coercion variable
+  | CoVarId    -- ^ A coercion variable
+               -- This only covers /un-lifted/ coercions, of type
+               -- (t1 ~# t2) or (t1 ~R# t2), not their lifted variants
 
 data RecSelParent = RecSelData TyCon | RecSelPatSyn PatSyn deriving Eq
   -- Either `TyCon` or `PatSyn` depending
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs
index 11a4dee340..d6bd609c4c 100644
--- a/compiler/basicTypes/Var.hs
+++ b/compiler/basicTypes/Var.hs
@@ -34,7 +34,7 @@
 
 module Var (
         -- * The main data type and synonyms
-        Var, CoVar, Id, DictId, DFunId, EvVar, EqVar, EvId, IpId,
+        Var, CoVar, Id, NcId, DictId, DFunId, EvVar, EqVar, EvId, IpId,
         TyVar, TypeVar, KindVar, TKVar, TyCoVar,
 
         -- ** Taking 'Var's apart
@@ -52,7 +52,7 @@ module Var (
 
         -- ** Predicates
         isId, isTKVar, isTyVar, isTcTyVar,
-        isLocalVar, isLocalId, isCoVar, isTyCoVar,
+        isLocalVar, isLocalId, isCoVar, isNonCoVarId, isTyCoVar,
         isGlobalId, isExportedId,
         mustHaveLocalBinding,
 
@@ -93,6 +93,14 @@ import Data.Data
 -}
 
 type Id    = Var       -- A term-level identifier
+                       --  predicate: isId
+
+type CoVar = Id        -- See Note [Evidence: EvIds and CoVars]
+                       --   predicate: isCoVar
+
+type NcId  = Id        -- A term-level (value) variable that is
+                       -- /not/ an (unlifted) coercion
+                       --    predicate: isNonCoVarId
 
 type TyVar   = Var     -- Type *or* kind variable (historical)
 
@@ -109,19 +117,19 @@ type DictId = EvId      -- A dictionary variable
 type IpId   = EvId      -- A term-level implicit parameter
 type EqVar  = EvId      -- Boxed equality evidence
 
-type CoVar = Id         -- See Note [Evidence: EvIds and CoVars]
-
 type TyCoVar = Id       -- Type, kind, *or* coercion variable
+                        --   predicate: isTyCoVar
 
-{-
-Note [Evidence: EvIds and CoVars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Evidence: EvIds and CoVars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * An EvId (evidence Id) is a term-level evidence variable
   (dictionary, implicit parameter, or equality). Could be boxed or unboxed.
 
 * DictId, IpId, and EqVar are synonyms when we know what kind of
   evidence we are talking about.  For example, an EqVar has type (t1 ~ t2).
 
+* A CoVar is always an un-lifted coercion, of type (t1 ~# t2) or (t1 ~R# t2)
+
 Note [Kind and type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Before kind polymorphism, TyVar were used to mean type variables. Now
@@ -433,15 +441,22 @@ isTcTyVar :: Var -> Bool
 isTcTyVar (TcTyVar {}) = True
 isTcTyVar _            = False
 
+isTyCoVar :: Var -> Bool
+isTyCoVar v = isTyVar v || isCoVar v
+
 isId :: Var -> Bool
 isId (Id {}) = True
 isId _       = False
 
-isTyCoVar :: Var -> Bool
-isTyCoVar v = isTyVar v || isCoVar v
-
 isCoVar :: Var -> Bool
-isCoVar v = isId v && isCoVarDetails (id_details v)
+-- A coercion variable
+isCoVar (Id { id_details = details }) = isCoVarDetails details
+isCoVar _                             = False
+
+isNonCoVarId :: Var -> Bool
+-- A term variable (Id) that is /not/ a coercion variable
+isNonCoVarId (Id { id_details = details }) = not (isCoVarDetails details)
+isNonCoVarId _                             = False
 
 isLocalId :: Var -> Bool
 isLocalId (Id { idScope = LocalId _ }) = True
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 9baf3fc008..ef44affd3e 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -584,7 +584,7 @@ lintCoreExpr :: CoreExpr -> LintM OutType
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintCoreExpr (Var var)
-  = do  { checkL (isId var && not (isCoVar var))
+  = do  { checkL (isNonCoVarId var)
                  (text "Non term variable" <+> ppr var)
 
         ; checkDeadIdOcc var
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index a31650969e..b4edfee593 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -110,7 +110,7 @@ import TysWiredIn
 data Subst
   = Subst InScopeSet  -- Variables in in scope (both Ids and TyVars) /after/
                       -- applying the substitution
-          IdSubstEnv  -- Substitution for Ids
+          IdSubstEnv  -- Substitution from NcIds to CoreExprs
           TvSubstEnv  -- Substitution from TyVars to Types
           CvSubstEnv  -- Substitution from CoVars to Coercions
 
@@ -180,7 +180,7 @@ TvSubstEnv and CvSubstEnv?
 -}
 
 -- | An environment for substituting for 'Id's
-type IdSubstEnv = IdEnv CoreExpr
+type IdSubstEnv = IdEnv CoreExpr   -- Domain is NcIds, i.e. not coercions
 
 ----------------------------
 isEmptySubst :: Subst -> Bool
@@ -209,11 +209,15 @@ zapSubstEnv (Subst in_scope _ _ _) = Subst in_scope emptyVarEnv emptyVarEnv empt
 -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
 extendIdSubst :: Subst -> Id -> CoreExpr -> Subst
 -- ToDo: add an ASSERT that fvs(subst-result) is already in the in-scope set
-extendIdSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope (extendVarEnv ids v r) tvs cvs
+extendIdSubst (Subst in_scope ids tvs cvs) v r
+  = ASSERT2( isNonCoVarId v, ppr v $$ ppr r )
+    Subst in_scope (extendVarEnv ids v r) tvs cvs
 
 -- | Adds multiple 'Id' substitutions to the 'Subst': see also 'extendIdSubst'
 extendIdSubstList :: Subst -> [(Id, CoreExpr)] -> Subst
-extendIdSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs cvs
+extendIdSubstList (Subst in_scope ids tvs cvs) prs
+  = ASSERT( all (isNonCoVarId . fst) prs )
+    Subst in_scope (extendVarEnvList ids prs) tvs cvs
 
 -- | Add a substitution for a 'TyVar' to the 'Subst'
 -- The 'TyVar' *must* be a real TyVar, and not a CoVar
diff --git a/compiler/simplCore/CSE.hs b/compiler/simplCore/CSE.hs
index 6a6cceb694..b4e6e14991 100644
--- a/compiler/simplCore/CSE.hs
+++ b/compiler/simplCore/CSE.hs
@@ -177,8 +177,10 @@ cseRhs env (id',rhs)
           | always_active -> (extendCSEnv env rhs' id', (zapped_id, rhs'))
           | otherwise     -> (env,                      (id', rhs'))
         Just id
-          | always_active -> (extendCSSubst env id' id, (id', mkTicks ticks $ varToCoreExpr id))
-          | otherwise     -> (env,                      (id', mkTicks ticks $ varToCoreExpr id))
+          | always_active -> (extendCSSubst env id' id_expr, (id', mkTicks ticks id_expr))
+          | otherwise     -> (env,                           (id', mkTicks ticks id_expr))
+          where
+            id_expr = varToCoreExpr id  -- Could be a CoVar
           -- In the Just case, we have
           --        x = rhs
           --        ...
@@ -252,10 +254,10 @@ cseAlts env scrut' bndr bndr' alts
     scrut'' = stripTicksTopE tickishFloatable scrut'
     (con_target, alt_env)
         = case scrut'' of
-            Var v' -> (v',     extendCSSubst env bndr v')    -- See Note [Case binders 1]
-                                                             -- map: bndr -> v'
+            Var v' -> (v', extendCSSubst env bndr scrut'') -- See Note [Case binders 1]
+                                                           -- map: bndr -> v'
 
-            _      ->  (bndr', extendCSEnv env scrut' bndr') -- See Note [Case binders 2]
+            _      -> (bndr', extendCSEnv env scrut' bndr') -- See Note [Case binders 2]
                                                              -- map: scrut' -> bndr'
 
     arg_tys = tyConAppArgs (idType bndr)
@@ -317,8 +319,8 @@ csEnvSubst = cs_subst
 lookupSubst :: CSEnv -> Id -> OutExpr
 lookupSubst (CS { cs_subst = sub}) x = lookupIdSubst (text "CSE.lookupSubst") sub x
 
-extendCSSubst :: CSEnv -> Id  -> Id -> CSEnv
-extendCSSubst cse x y = cse { cs_subst = extendIdSubst (cs_subst cse) x (Var y) }
+extendCSSubst :: CSEnv -> Id  -> CoreExpr -> CSEnv
+extendCSSubst cse x rhs = cse { cs_subst = extendSubst (cs_subst cse) x rhs }
 
 addBinder :: CSEnv -> Var -> (CSEnv, Var)
 addBinder cse v = (cse { cs_subst = sub' }, v')
diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index 477092e09b..09caa0034d 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -1220,7 +1220,7 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
               -> SpecM (Maybe ((Id,CoreExpr),     -- Specialised definition
                                UsageDetails,      -- Usage details from specialised body
                                CoreRule))         -- Info for the Id's SpecEnv
-    spec_call (CallKey call_ts, (call_ds, _))
+    spec_call _call_info@(CallKey call_ts, (call_ds, _))
       = ASSERT( call_ts `lengthIs` n_tyvars  && call_ds `lengthIs` n_dicts )
 
         -- Suppose f's defn is  f = /\ a b c -> \ d1 d2 -> rhs
@@ -1250,13 +1250,17 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
            ; let (rhs_env2, dx_binds, spec_dict_args)
                             = bindAuxiliaryDicts rhs_env rhs_dict_ids call_ds inst_dict_ids
                  ty_args    = mk_ty_args call_ts poly_tyvars
-                 rule_args  = ty_args ++ map Var inst_dict_ids
+                 rule_args  = ty_args ++ map varToCoreExpr inst_dict_ids
+                                -- varToCoreExpr does the right thing for CoVars
                  rule_bndrs = poly_tyvars ++ inst_dict_ids
 
            ; dflags <- getDynFlags
            ; if already_covered dflags rule_args then
                 return Nothing
-             else do
+             else -- pprTrace "spec_call" (vcat [ ppr _call_info, ppr fn, ppr rhs_dict_ids
+                  --                           , text "rhs_env2" <+> ppr (se_subst rhs_env2)
+                  --                           , ppr dx_binds ]) $
+                  do
            {    -- Figure out the type of the specialised function
              let body_ty = applyTypeToArgs rhs fn_type rule_args
                  (lam_args, app_args)           -- Add a dummy argument if body_ty is unlifted
@@ -1365,7 +1369,7 @@ bindAuxiliaryDicts env@(SE { se_subst = subst, se_interesting = interesting })
   = (env', dx_binds, spec_dict_args)
   where
     (dx_binds, spec_dict_args) = go call_ds inst_dict_ids
-    env' = env { se_subst = subst `CoreSubst.extendIdSubstList`
+    env' = env { se_subst = subst `CoreSubst.extendSubstList`
                                      (orig_dict_ids `zip` spec_dict_args)
                                   `CoreSubst.extendInScopeList` dx_ids
                , se_interesting = interesting `unionVarSet` interesting_dicts }
@@ -1905,6 +1909,8 @@ whole it's only a small win: 2.2% improvement in allocation for ansi,
 
 interestingDict :: SpecEnv -> CoreExpr -> Bool
 -- A dictionary argument is interesting if it has *some* structure
+-- NB: "dictionary" arguments include constraints of all sorts,
+--     including equality constraints; hence the Coercion case
 interestingDict env (Var v) =  hasSomeUnfolding (idUnfolding v)
                             || isDataConWorkId v
                             || v `elemVarSet` se_interesting env
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 9686531533..0a5436fcf6 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -525,7 +525,9 @@ mkFunTys tys ty = foldr mkFunTy ty tys
 mkForAllTys :: [TyBinder] -> Type -> Type
 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 
--- | Does this type classify a core Coercion?
+-- | Does this type classify a core (unlifted) Coercion?
+-- At either role nominal or reprsentational
+--    (t1 ~# t2) or (t1 ~R# t2)
 isCoercionType :: Type -> Bool
 isCoercionType (TyConApp tc tys)
   | (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
diff --git a/testsuite/tests/simplCore/should_compile/T11644.hs b/testsuite/tests/simplCore/should_compile/T11644.hs
new file mode 100644
index 0000000000..e0d020dcf9
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T11644.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeFamilies, ScopedTypeVariables#-}
+
+module T11644 where
+
+class Foo m where
+    type Bar m :: *
+    action :: m -> Bar m -> m
+
+right x m = action m (Right x)
+
+right' :: (Either a b ~ Bar m, Foo m) => b -> m -> m
+right' x m = action m (Right x)
+
+instance Foo Int where
+    type Bar Int = Either Int Int
+    action m a = either (*) (+) a m
+
+instance Foo Float where
+    type Bar Float = Either Float Float
+    action m a = either (*) (+) a m
+
+foo = print $ right (1::Int) (3 :: Int)
+bar = print $ right (1::Float) (3 :: Float)
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 9d88237b66..9f3af8b192 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -231,3 +231,4 @@ test('T11155',
 test('T11232', normal, compile, ['-O2'])
 test('T11562', normal, compile, ['-O2'])
 test('T11742', normal, compile, ['-O2'])
+test('T11644', normal, compile, ['-O2'])