Docs: datacon eta-expansion, rep-poly checks

The existing notes weren't very clear on how the eta-expansion of
data constructors that occurs in tcInferDataCon/dsConLike interacts
with the representation polymorphism invariants. So we explain with
a few more details how we ensure that the representation-polymorphic
lambdas introduced by tcInferDataCon/dsConLike don't end up causing
problems, by checking they are properly instantiated and then relying
on the simple optimiser to perform beta reduction.

A few additional changes:

  - ConLikeTc just take type variables instead of binders, as we
    never actually used the binders.
  - Removed the FRRApp constructor of FRROrigin; it was no longer used
    now that we use ExpectedFunTyOrigin.
  - Adds a bit of documentation to the constructors
    of ExpectedFunTyOrigin.

8 files changed, 111 insertions, 37 deletions

diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 6020950c11..a4960ca555 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -52,7 +52,6 @@ import GHC.Types.Fixity
 import GHC.Types.SourceText
 import GHC.Types.SrcLoc
 import GHC.Types.Tickish (CoreTickish)
-import GHC.Types.Var( InvisTVBinder )
 import GHC.Core.ConLike
 import GHC.Unit.Module (ModuleName)
 import GHC.Utils.Misc
@@ -62,7 +61,7 @@ import GHC.Utils.Panic.Plain
 import GHC.Data.FastString
 import GHC.Core.Type
 import GHC.Builtin.Types (mkTupleStr)
-import GHC.Tc.Utils.TcType (TcType)
+import GHC.Tc.Utils.TcType (TcType, TcTyVar)
 import {-# SOURCE #-} GHC.Tc.Types (TcLclEnv)
 
 -- libraries:
@@ -507,7 +506,7 @@ data XXExprGhcTc
                    --     GHC.Tc.Gen.Head
                    -- The two arguments describe how to eta-expand
                    -- the data constructor when desugaring
-        ConLike [InvisTVBinder] [Scaled TcType]
+        ConLike [TcTyVar] [Scaled TcType]
 
   ---------------------------------------
   -- Haskell program coverage (Hpc) Support
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index e7d2d58d66..565338d5a7 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -1033,11 +1033,11 @@ dsHsConLike (PatSynCon ps)
   | otherwise
   = pprPanic "dsConLike" (ppr ps)
 
-dsConLike :: ConLike -> [TcInvisTVBinder] -> [Scaled Type] -> DsM CoreExpr
+dsConLike :: ConLike -> [TcTyVar] -> [Scaled Type] -> DsM CoreExpr
 -- This function desugars ConLikeTc
 -- See Note [Typechecking data constructors] in GHC.Tc.Gen.Head
 --     for what is going on here
-dsConLike con tvbs tys
+dsConLike con tvs tys
   = do { ds_con <- dsHsConLike con
        ; ids    <- newSysLocalsDs tys
                    -- newSysLocalDs: /can/ be lev-poly; see
@@ -1046,7 +1046,6 @@ dsConLike con tvbs tys
                  ds_con `mkTyApps` mkTyVarTys tvs
                         `mkVarApps` drop_stupid ids) }
   where
-    tvs = binderVars tvbs
 
     drop_stupid = dropList (conLikeStupidTheta con)
     -- drop_stupid: see Note [Instantiating stupid theta]
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index c2df311b30..05d4a25dc2 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -406,12 +406,12 @@ function arguments. See Note [Representation polymorphism invariants]
 in GHC.Core.  That is checked by the calls to `hasFixedRuntimeRep ` in
 `tcEValArg`.
 
-But some /built-in/ functions are representation-polymorphic.  Users
-can't define such Ids; they are all GHC built-ins or data
+But some /built-in/ functions have representation-polymorphic argument
+types. Users can't define such Ids; they are all GHC built-ins or data
 constructors.  Specifically they are:
 
 1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings.
-2. Primops, such as raise#
+2. Primops, such as raise#.
 3. Newtype constructors with `UnliftedNewtypes` that have
    a representation-polymorphic argument.
 4. Representation-polymorphic data constructors: unboxed tuples
@@ -480,7 +480,10 @@ Wrinkles
 
   Because we want to accept this, we switch off Lint's representation
   polymorphism checks when Lint checks the output of the desugarer;
-  see the lf_check_fixed_repy flag in GHC.Core.Lint.lintCoreBindings.
+  see the lf_check_fixed_rep flag in GHC.Core.Lint.lintCoreBindings.
+
+  We then rely on the simple optimiser to beta reduce these
+  representation-polymorphic lambdas (e.g. GHC.Core.SimpleOpt.simple_app).
 
 * Arity.  We don't want to check for arguments past the
   arity of the function.  For example
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 3028f540d9..0212966934 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -809,7 +809,8 @@ check_naughty lbl id
 tcInferDataCon :: DataCon -> TcM (HsExpr GhcTc, TcSigmaType)
 -- See Note [Typechecking data constructors]
 tcInferDataCon con
-  = do { let tvs   = dataConUserTyVarBinders con
+  = do { let tvbs  = dataConUserTyVarBinders con
+             tvs   = binderVars tvbs
              theta = dataConOtherTheta con
              args  = dataConOrigArgTys con
              res   = dataConOrigResTy con
@@ -823,7 +824,7 @@ tcInferDataCon con
                 -- See Note [Instantiating stupid theta]
 
        ; return ( XExpr (ConLikeTc (RealDataCon con) tvs all_arg_tys)
-                , mkInvisForAllTys tvs $ mkPhiTy full_theta $
+                , mkInvisForAllTys tvbs $ mkPhiTy full_theta $
                   mkVisFunTys scaled_arg_tys res ) }
   where
     linear_to_poly :: Scaled Type -> TcM (Scaled Type)
@@ -874,7 +875,7 @@ mostly in tcInferDataCon:
 
 4. The (ConLikeTc K [r,a] [Scaled p a]) is later desugared by
    GHC.HsToCore.Expr.dsConLike to:
-     (/\r a. \(x %p :: a). K @r @a x)
+     (/\r (a :: TYPE r). \(x %p :: a). K @r @a x)
    which has the desired type given in the previous bullet.
    The 'p' is the multiplicity unification variable, which
    will by now have been unified to something, or defaulted in
@@ -883,21 +884,37 @@ mostly in tcInferDataCon:
 
 Wrinkles
 
-* Why put [InvisTVBinder] in ConLikeTc, when we only need [TyVar] to
-  desugar?  It's a bit of a toss-up, but having [InvisTvBinder] supports
-  a future hsExprType :: HsExpr GhcTc -> Type
-
-* Note that the [InvisTvBinder] is strictly redundant anyway; it's
-  just the dataConUserTyVarBinders of the data constructor.  Similarly
-  in the [Scaled TcType] field of ConLikeTc, the type comes directly
+* Note that the [TcType] is strictly redundant anyway; those are the
+  type variables from the dataConUserTyVarBinders of the data constructor.
+  Similarly in the [Scaled TcType] field of ConLikeTc, the types come directly
   from the data constructor.  The only bit that /isn't/ redundant is the
   fresh multiplicity variables!
 
   So an alternative would be to define ConLikeTc like this:
       | ConLikeTc [TcType]    -- Just the multiplicity variables
-  But then the desugarer (and hsExprType, when we implement it) would
-  need to repeat some of the work done here.  So for now at least
-  ConLikeTc records this strictly-redundant info.
+  But then the desugarer would need to repeat some of the work done here.
+  So for now at least ConLikeTc records this strictly-redundant info.
+
+* The lambda expression we produce in (4) can have representation-polymorphic
+  arguments, as indeed in (/\r (a :: TYPE r). \(x %p :: a). K @r @a x),
+  we have a lambda-bound variable x :: (a :: TYPE r).
+  This goes against the representation polymorphism invariants given in
+  Note [Representation polymorphism invariants] in GHC.Core. The trick is that
+  this this lambda will always be instantiated in a way that upholds the invariants.
+  This is achieved as follows:
+
+    A. Any arguments to such lambda abstractions are guaranteed to have
+       a fixed runtime representation. This is enforced in 'tcApp' by
+       'matchActualFunTySigma'.
+
+    B. If there are fewer arguments than there are bound term variables,
+       hasFixedRuntimeRep_remainingValArgs will ensure that we are still
+       instantiating at a representation-monomorphic type, e.g.
+
+       ( /\r (a :: TYPE r). \ (x %p :: a). K @r @a x) @IntRep @Int#
+         :: Int# -> T IntRep Int#
+
+  We then rely on the simple optimiser to beta reduce the lambda.
 
 * See Note [Instantiating stupid theta] for an extra wrinkle
 
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 82dbafcdf1..54a0f2127e 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -979,15 +979,10 @@ producing an error message of the form:
 -- | In what context are we checking that a type has a fixed runtime representation?
 data FRROrigin
 
-  -- | Function arguments must have a fixed runtime representation.
-  --
-  -- Test case: RepPolyApp.
-  = FRRApp !(HsExpr GhcTc)
-
   -- | Record fields in record updates must have a fixed runtime representation.
   --
   -- Test case: RepPolyRecordUpdate.
-  | FRRRecordUpdate !RdrName !(HsExpr GhcTc)
+  = FRRRecordUpdate !RdrName !(HsExpr GhcTc)
 
   -- | Variable binders must have a fixed runtime representation.
   --
@@ -1073,9 +1068,6 @@ data FRROrigin
 -- Note that this function does not include the specific 'RuntimeRep'
 -- which is not fixed. That information is added by 'GHC.Tc.Errors.mkFRRErr'.
 pprFRROrigin :: FRROrigin -> SDoc
-pprFRROrigin (FRRApp arg)
-  = sep [ text "The function argument"
-        , nest 2 $ quotes (ppr arg) ]
 pprFRROrigin (FRRRecordUpdate lbl _arg)
   = sep [ text "The record update at field"
         , quotes (ppr lbl) ]
@@ -1241,8 +1233,28 @@ instance Outputable FRRArrowOrigin where
 --     Uses 'pprExpectedFunTyOrigin'.
 --     See 'FRROrigin' for more general origins of representation polymorphism checks.
 data ExpectedFunTyOrigin
-  = ExpectedFunTySyntaxOp !CtOrigin !(HsExpr GhcRn)
-  | ExpectedFunTyViewPat  !(HsExpr GhcRn)
+
+  -- | A rebindable syntax operator is expected to have a function type.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyDoBind, RepPolyDoBody{1,2}, RepPolyMc{Bind,Body,Guard}, RepPolyNPlusK
+  = ExpectedFunTySyntaxOp
+    !CtOrigin
+    !(HsExpr GhcRn)
+      -- ^ rebindable syntax operator
+
+  -- | A view pattern must have a function type.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyBinder
+  | ExpectedFunTyViewPat
+    !(HsExpr GhcRn)
+      -- ^ function used in the view pattern
+
+  -- | Need to be able to extract an argument type from a function type.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyApp
   | forall (p :: Pass)
       . (OutputableBndrId p)
       => ExpectedFunTyArg
@@ -1250,9 +1262,33 @@ data ExpectedFunTyOrigin
             -- ^ function
           !(HsExpr (GhcPass p))
             -- ^ argument
-  | ExpectedFunTyMatches  !TypedThing !(MatchGroup GhcRn (LHsExpr GhcRn))
-  | ExpectedFunTyLam      !(MatchGroup GhcRn (LHsExpr GhcRn))
-  | ExpectedFunTyLamCase  LamCaseVariant !(HsExpr GhcRn)
+
+  -- | Ensure that a function defined by equations indeed has a function type
+  -- with the appropriate number of arguments.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyBinder, RepPolyRecordPattern, RepPolyWildcardPattern
+  | ExpectedFunTyMatches
+      !TypedThing
+        -- ^ name of the function
+      !(MatchGroup GhcRn (LHsExpr GhcRn))
+       -- ^ equations
+
+  -- | Ensure that a lambda abstraction has a function type.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyLambda
+  | ExpectedFunTyLam
+      !(MatchGroup GhcRn (LHsExpr GhcRn))
+
+  -- | Ensure that a lambda case expression has a function type.
+  --
+  -- Test cases for representation-polymorphism checks:
+  --   RepPolyMatch
+  | ExpectedFunTyLamCase
+      LamCaseVariant
+      !(HsExpr GhcRn)
+       -- ^ the entire lambda-case expression
 
 pprExpectedFunTyOrigin :: ExpectedFunTyOrigin
                        -> Int -- ^ argument position (starting at 1)
diff --git a/testsuite/tests/rep-poly/RepPolyLambda.hs b/testsuite/tests/rep-poly/RepPolyLambda.hs
new file mode 100644
index 0000000000..8164a90fbb
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyLambda.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module RepPolyLambda where
+
+import Data.Kind
+import GHC.Exts
+
+f :: forall r (a :: TYPE r). a -> a
+f = \ x -> x
diff --git a/testsuite/tests/rep-poly/RepPolyLambda.stderr b/testsuite/tests/rep-poly/RepPolyLambda.stderr
new file mode 100644
index 0000000000..d655354548
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyLambda.stderr
@@ -0,0 +1,8 @@
+
+RepPolyLambda.hs:11:5: error:
+    • The binder of the lambda expression
+      does not have a fixed runtime representation.
+      Its type is:
+        a :: TYPE r
+    • In the expression: \ x -> x
+      In an equation for ‘f’: f = \ x -> x
diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T
index e97ae78192..140076e598 100644
--- a/testsuite/tests/rep-poly/all.T
+++ b/testsuite/tests/rep-poly/all.T
@@ -47,6 +47,7 @@ test('RepPolyDoBody1', normal, compile_fail, [''])
 test('RepPolyDoBody2', normal, compile_fail, [''])
 test('RepPolyDoReturn', normal, compile, [''])
 test('RepPolyFFI', normal, compile, [''])
+test('RepPolyLambda', normal, compile_fail, [''])
 test('RepPolyLeftSection1', normal, compile, [''])
 test('RepPolyLeftSection2', normal, compile_fail, [''])
 test('RepPolyMagic', normal, compile_fail, [''])