Fix #13233 by checking for lev-poly primops

The implementation plan is all in Note [Detecting forced eta expansion]
in DsExpr.

Test Plan: ./validate, codeGen/should_fail/T13233

Reviewers: simonpj, austin, bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13233

Differential Revision: https://phabricator.haskell.org/D3490

18 files changed, 269 insertions, 154 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 8182272be7..0888afbeeb 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1350,8 +1350,8 @@ lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
 -- See Note [GHC Formalism]
 lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                        -- or lintarrow "coercion `blah'" k1 k2
-  = do { unless (okArrowArgKind k1)    (addErrL (msg (text "argument") k1))
-       ; unless (okArrowResultKind k2) (addErrL (msg (text "result")   k2))
+  = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
+       ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result")   k2))
        ; return liftedTypeKind }
   where
     msg ar k
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index b5e97f7fa7..a669437c68 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -457,7 +457,8 @@ See #case_invariants#
 
 Note [Levity polymorphism invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The levity-polymorphism invariants are these:
+The levity-polymorphism invariants are these (as per "Levity Polymorphism",
+PLDI '17):
 
 * The type of a term-binder must not be levity-polymorphic,
   unless it is a let(rec)-bound join point
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index c08353a15b..1b02502a31 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -580,7 +580,7 @@ translatePat fam_insts pat = case pat of
     | otherwise -> do
         ps      <- translatePat fam_insts p
         (xp,xe) <- mkPmId2Forms ty
-        let g = mkGuard ps (HsWrap wrapper (unLoc xe))
+        let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
         return [xp,g]
 
   -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
diff --git a/compiler/deSugar/DsArrows.hs b/compiler/deSugar/DsArrows.hs
index c3be55504b..4fe43eb1c0 100644
--- a/compiler/deSugar/DsArrows.hs
+++ b/compiler/deSugar/DsArrows.hs
@@ -575,8 +575,8 @@ dsCmd ids local_vars stack_ty res_ty
     let
         left_id  = HsConLikeOut (RealDataCon left_con)
         right_id = HsConLikeOut (RealDataCon right_con)
-        left_expr  ty1 ty2 e = noLoc $ HsApp (noLoc $ HsWrap (mkWpTyApps [ty1, ty2]) left_id ) e
-        right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ HsWrap (mkWpTyApps [ty1, ty2]) right_id) e
+        left_expr  ty1 ty2 e = noLoc $ HsApp (noLoc $ mkHsWrap (mkWpTyApps [ty1, ty2]) left_id ) e
+        right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ mkHsWrap (mkWpTyApps [ty1, ty2]) right_id) e
 
         -- Prefix each tuple with a distinct series of Left's and Right's,
         -- in a balanced way, keeping track of the types.
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index 39f76ea2c0..d4a96e6f3f 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -252,27 +252,33 @@ dsLExprNoLP (L loc e)
        ; return e' }
 
 dsExpr :: HsExpr Id -> DsM CoreExpr
-dsExpr (HsPar e)              = dsLExpr e
-dsExpr (ExprWithTySigOut e _) = dsLExpr e
-dsExpr (HsVar (L _ var))      = return (varToCoreExpr var)
-                                -- See Note [Desugaring vars]
-dsExpr (HsUnboundVar {})      = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them
-dsExpr (HsConLikeOut con)     = return (dsConLike con)
-dsExpr (HsIPVar _)            = panic "dsExpr: HsIPVar"
-dsExpr (HsOverLabel{})        = panic "dsExpr: HsOverLabel"
-dsExpr (HsLit lit)            = dsLit lit
-dsExpr (HsOverLit lit)        = dsOverLit lit
-
-dsExpr (HsWrap co_fn e)
-  = do { e' <- dsExpr e
+dsExpr = ds_expr False
+
+ds_expr :: Bool   -- are we directly inside an HsWrap?
+                  -- See Wrinkle in Note [Detecting forced eta expansion]
+        -> HsExpr Id -> DsM CoreExpr
+ds_expr _ (HsPar e)              = dsLExpr e
+ds_expr _ (ExprWithTySigOut e _) = dsLExpr e
+ds_expr w (HsVar (L _ var))      = dsHsVar w var
+ds_expr _ (HsUnboundVar {})      = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them
+ds_expr w (HsConLikeOut con)     = dsConLike w con
+ds_expr _ (HsIPVar _)            = panic "dsExpr: HsIPVar"
+ds_expr _ (HsOverLabel{})        = panic "dsExpr: HsOverLabel"
+ds_expr _ (HsLit lit)            = dsLit lit
+ds_expr _ (HsOverLit lit)        = dsOverLit lit
+
+ds_expr _ (HsWrap co_fn e)
+  = do { e' <- ds_expr True e
        ; wrap' <- dsHsWrapper co_fn
        ; dflags <- getDynFlags
        ; let wrapped_e = wrap' e'
-       ; warnAboutIdentities dflags e' (exprType wrapped_e)
+             wrapped_ty = exprType wrapped_e
+       ; checkForcedEtaExpansion e wrapped_ty -- See Note [Detecting forced eta expansion]
+       ; warnAboutIdentities dflags e' wrapped_ty
        ; return wrapped_e }
 
-dsExpr (NegApp (L loc (HsOverLit lit@(OverLit { ol_val = HsIntegral src i })))
-                neg_expr)
+ds_expr _ (NegApp (L loc (HsOverLit lit@(OverLit { ol_val = HsIntegral src i })))
+                  neg_expr)
   = do { expr' <- putSrcSpanDs loc $ do
           { dflags <- getDynFlags
           ; warnAboutOverflowedLiterals dflags
@@ -280,23 +286,23 @@ dsExpr (NegApp (L loc (HsOverLit lit@(OverLit { ol_val = HsIntegral src i })))
           ; dsOverLit' dflags lit }
        ; dsSyntaxExpr neg_expr [expr'] }
 
-dsExpr (NegApp expr neg_expr)
+ds_expr _ (NegApp expr neg_expr)
   = do { expr' <- dsLExpr expr
        ; dsSyntaxExpr neg_expr [expr'] }
 
-dsExpr (HsLam a_Match)
+ds_expr _ (HsLam a_Match)
   = uncurry mkLams <$> matchWrapper LambdaExpr Nothing a_Match
 
-dsExpr (HsLamCase matches)
+ds_expr _ (HsLamCase matches)
   = do { ([discrim_var], matching_code) <- matchWrapper CaseAlt Nothing matches
        ; return $ Lam discrim_var matching_code }
 
-dsExpr e@(HsApp fun arg)
+ds_expr _ e@(HsApp fun arg)
   = do { fun' <- dsLExpr fun
        ; dsWhenNoErrs (dsLExprNoLP arg)
                       (\arg' -> mkCoreAppDs (text "HsApp" <+> ppr e) fun' arg') }
 
-dsExpr (HsAppTypeOut e _)
+ds_expr _ (HsAppTypeOut e _)
     -- ignore type arguments here; they're in the wrappers instead at this point
   = dsLExpr e
 
@@ -340,19 +346,19 @@ If \tr{expr} is actually just a variable, say, then the simplifier
 will sort it out.
 -}
 
-dsExpr e@(OpApp e1 op _ e2)
+ds_expr _ e@(OpApp e1 op _ e2)
   = -- for the type of y, we need the type of op's 2nd argument
     do { op' <- dsLExpr op
        ; dsWhenNoErrs (mapM dsLExprNoLP [e1, e2])
                       (\exprs' -> mkCoreAppsDs (text "opapp" <+> ppr e) op' exprs') }
 
-dsExpr (SectionL expr op)       -- Desugar (e !) to ((!) e)
+ds_expr _ (SectionL expr op)       -- Desugar (e !) to ((!) e)
   = do { op' <- dsLExpr op
        ; dsWhenNoErrs (dsLExprNoLP expr)
                       (\expr' -> mkCoreAppDs (text "sectionl" <+> ppr expr) op' expr') }
 
 -- dsLExpr (SectionR op expr)   -- \ x -> op x expr
-dsExpr e@(SectionR op expr) = do
+ds_expr _ e@(SectionR op expr) = do
     core_op <- dsLExpr op
     -- for the type of x, we need the type of op's 2nd argument
     let (x_ty:y_ty:_, _) = splitFunTys (exprType core_op)
@@ -363,7 +369,7 @@ dsExpr e@(SectionR op expr) = do
                                    Lam x_id (mkCoreAppsDs (text "sectionr" <+> ppr e)
                                                           core_op [Var x_id, Var y_id]))
 
-dsExpr (ExplicitTuple tup_args boxity)
+ds_expr _ (ExplicitTuple tup_args boxity)
   = do { let go (lam_vars, args) (L _ (Missing ty))
                     -- For every missing expression, we need
                     -- another lambda in the desugaring.
@@ -381,14 +387,14 @@ dsExpr (ExplicitTuple tup_args boxity)
        ; return $ mkCoreLams lam_vars $
                   mkCoreTupBoxity boxity args }
 
-dsExpr (ExplicitSum alt arity expr types)
+ds_expr _ (ExplicitSum alt arity expr types)
   = do { core_expr <- dsLExpr expr
        ; return $ mkCoreConApps (sumDataCon alt arity)
                                 (map (Type . getRuntimeRep "dsExpr ExplicitSum") types ++
                                  map Type types ++
                                  [core_expr]) }
 
-dsExpr (HsSCC _ cc expr@(L loc _)) = do
+ds_expr _ (HsSCC _ cc expr@(L loc _)) = do
     dflags <- getDynFlags
     if gopt Opt_SccProfilingOn dflags
       then do
@@ -399,31 +405,31 @@ dsExpr (HsSCC _ cc expr@(L loc _)) = do
                <$> dsLExpr expr
       else dsLExpr expr
 
-dsExpr (HsCoreAnn _ _ expr)
+ds_expr _ (HsCoreAnn _ _ expr)
   = dsLExpr expr
 
-dsExpr (HsCase discrim matches)
+ds_expr _ (HsCase discrim matches)
   = do { core_discrim <- dsLExpr discrim
        ; ([discrim_var], matching_code) <- matchWrapper CaseAlt (Just discrim) matches
        ; return (bindNonRec discrim_var core_discrim matching_code) }
 
 -- Pepe: The binds are in scope in the body but NOT in the binding group
 --       This is to avoid silliness in breakpoints
-dsExpr (HsLet binds body) = do
+ds_expr _ (HsLet binds body) = do
     body' <- dsLExpr body
     dsLocalBinds binds body'
 
 -- We need the `ListComp' form to use `deListComp' (rather than the "do" form)
 -- because the interpretation of `stmts' depends on what sort of thing it is.
 --
-dsExpr (HsDo ListComp     (L _ stmts) res_ty) = dsListComp stmts res_ty
-dsExpr (HsDo PArrComp     (L _ stmts) _)      = dsPArrComp (map unLoc stmts)
-dsExpr (HsDo DoExpr       (L _ stmts) _)      = dsDo stmts
-dsExpr (HsDo GhciStmtCtxt (L _ stmts) _)      = dsDo stmts
-dsExpr (HsDo MDoExpr      (L _ stmts) _)      = dsDo stmts
-dsExpr (HsDo MonadComp    (L _ stmts) _)      = dsMonadComp stmts
-
-dsExpr (HsIf mb_fun guard_expr then_expr else_expr)
+ds_expr _ (HsDo ListComp     (L _ stmts) res_ty) = dsListComp stmts res_ty
+ds_expr _ (HsDo PArrComp     (L _ stmts) _)      = dsPArrComp (map unLoc stmts)
+ds_expr _ (HsDo DoExpr       (L _ stmts) _)      = dsDo stmts
+ds_expr _ (HsDo GhciStmtCtxt (L _ stmts) _)      = dsDo stmts
+ds_expr _ (HsDo MDoExpr      (L _ stmts) _)      = dsDo stmts
+ds_expr _ (HsDo MonadComp    (L _ stmts) _)      = dsMonadComp stmts
+
+ds_expr _ (HsIf mb_fun guard_expr then_expr else_expr)
   = do { pred <- dsLExpr guard_expr
        ; b1 <- dsLExpr then_expr
        ; b2 <- dsLExpr else_expr
@@ -431,7 +437,7 @@ dsExpr (HsIf mb_fun guard_expr then_expr else_expr)
            Just fun -> dsSyntaxExpr fun [pred, b1, b2]
            Nothing  -> return $ mkIfThenElse pred b1 b2 }
 
-dsExpr (HsMultiIf res_ty alts)
+ds_expr _ (HsMultiIf res_ty alts)
   | null alts
   = mkErrorExpr
 
@@ -450,16 +456,16 @@ dsExpr (HsMultiIf res_ty alts)
              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -}
 
-dsExpr (ExplicitList elt_ty wit xs)
+ds_expr _ (ExplicitList elt_ty wit xs)
   = dsExplicitList elt_ty wit xs
 
 -- We desugar [:x1, ..., xn:] as
 --   singletonP x1 +:+ ... +:+ singletonP xn
 --
-dsExpr (ExplicitPArr ty []) = do
+ds_expr _ (ExplicitPArr ty []) = do
     emptyP <- dsDPHBuiltin emptyPVar
     return (Var emptyP `App` Type ty)
-dsExpr (ExplicitPArr ty xs) = do
+ds_expr _ (ExplicitPArr ty xs) = do
     singletonP <- dsDPHBuiltin singletonPVar
     appP       <- dsDPHBuiltin appPVar
     xs'        <- mapM dsLExprNoLP xs
@@ -468,19 +474,19 @@ dsExpr (ExplicitPArr ty xs) = do
 
     return . foldr1 (binary appP) $ map (unary singletonP) xs'
 
-dsExpr (ArithSeq expr witness seq)
+ds_expr _ (ArithSeq expr witness seq)
   = case witness of
      Nothing -> dsArithSeq expr seq
      Just fl -> do { newArithSeq <- dsArithSeq expr seq
                    ; dsSyntaxExpr fl [newArithSeq] }
 
-dsExpr (PArrSeq expr (FromTo from to))
+ds_expr _ (PArrSeq expr (FromTo from to))
   = mkApps <$> dsExpr expr <*> mapM dsLExprNoLP [from, to]
 
-dsExpr (PArrSeq expr (FromThenTo from thn to))
+ds_expr _ (PArrSeq expr (FromThenTo from thn to))
   = mkApps <$> dsExpr expr <*> mapM dsLExprNoLP [from, thn, to]
 
-dsExpr (PArrSeq _ _)
+ds_expr _ (PArrSeq _ _)
   = panic "DsExpr.dsExpr: Infinite parallel array!"
     -- the parser shouldn't have generated it and the renamer and typechecker
     -- shouldn't have let it through
@@ -496,7 +502,7 @@ See Note [Grand plan for static forms] in StaticPtrTable for an overview.
     g = ... makeStatic loc f ...
 -}
 
-dsExpr (HsStatic _ expr@(L loc _)) = do
+ds_expr _ (HsStatic _ expr@(L loc _)) = do
     expr_ds <- dsLExprNoLP expr
     let ty = exprType expr_ds
     makeStaticId <- dsLookupGlobalId makeStaticName
@@ -538,8 +544,8 @@ We also handle @C{}@ as valid construction syntax for an unlabelled
 constructor @C@, setting all of @C@'s fields to bottom.
 -}
 
-dsExpr (RecordCon { rcon_con_expr = con_expr, rcon_flds = rbinds
-                  , rcon_con_like = con_like })
+ds_expr _ (RecordCon { rcon_con_expr = con_expr, rcon_flds = rbinds
+                     , rcon_con_like = con_like })
   = do { con_expr' <- dsExpr con_expr
        ; let
              (arg_tys, _) = tcSplitFunTys (exprType con_expr')
@@ -597,10 +603,10 @@ So we need to cast (T a Int) to (T a b).  Sigh.
 
 -}
 
-dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
-                       , rupd_cons = cons_to_upd
-                       , rupd_in_tys = in_inst_tys, rupd_out_tys = out_inst_tys
-                       , rupd_wrap = dict_req_wrap } )
+ds_expr _ expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
+                          , rupd_cons = cons_to_upd
+                          , rupd_in_tys = in_inst_tys, rupd_out_tys = out_inst_tys
+                          , rupd_wrap = dict_req_wrap } )
   | null fields
   = dsLExpr record_expr
   | otherwise
@@ -664,7 +670,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                  mk_val_arg fl pat_arg_id
                      = nlHsVar (lookupNameEnv upd_fld_env (flSelector fl) `orElse` pat_arg_id)
 
-                 inst_con = noLoc $ HsWrap wrap (HsConLikeOut con)
+                 inst_con = noLoc $ mkHsWrap wrap (HsConLikeOut con)
                         -- Reconstruct with the WrapId so that unpacking happens
                  -- The order here is because of the order in `TcPatSyn`.
                  wrap = mkWpEvVarApps theta_vars                                <.>
@@ -716,16 +722,16 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
 
 -- Template Haskell stuff
 
-dsExpr (HsRnBracketOut _ _) = panic "dsExpr HsRnBracketOut"
-dsExpr (HsTcBracketOut x ps) = dsBracket x ps
-dsExpr (HsSpliceE s)  = pprPanic "dsExpr:splice" (ppr s)
+ds_expr _ (HsRnBracketOut _ _) = panic "dsExpr HsRnBracketOut"
+ds_expr _ (HsTcBracketOut x ps) = dsBracket x ps
+ds_expr _ (HsSpliceE s)  = pprPanic "dsExpr:splice" (ppr s)
 
 -- Arrow notation extension
-dsExpr (HsProc pat cmd) = dsProcExpr pat cmd
+ds_expr _ (HsProc pat cmd) = dsProcExpr pat cmd
 
 -- Hpc Support
 
-dsExpr (HsTick tickish e) = do
+ds_expr _ (HsTick tickish e) = do
   e' <- dsLExpr e
   return (Tick tickish e')
 
@@ -736,30 +742,30 @@ dsExpr (HsTick tickish e) = do
 -- (did you go here: YES or NO), but will effect accurate
 -- tick counting.
 
-dsExpr (HsBinTick ixT ixF e) = do
+ds_expr _ (HsBinTick ixT ixF e) = do
   e2 <- dsLExpr e
   do { ASSERT(exprType e2 `eqType` boolTy)
        mkBinaryTickBox ixT ixF e2
      }
 
-dsExpr (HsTickPragma _ _ _ expr) = do
+ds_expr _ (HsTickPragma _ _ _ expr) = do
   dflags <- getDynFlags
   if gopt Opt_Hpc dflags
     then panic "dsExpr:HsTickPragma"
     else dsLExpr expr
 
 -- HsSyn constructs that just shouldn't be here:
-dsExpr (ExprWithTySig {})  = panic "dsExpr:ExprWithTySig"
-dsExpr (HsBracket     {})  = panic "dsExpr:HsBracket"
-dsExpr (HsArrApp      {})  = panic "dsExpr:HsArrApp"
-dsExpr (HsArrForm     {})  = panic "dsExpr:HsArrForm"
-dsExpr (EWildPat      {})  = panic "dsExpr:EWildPat"
-dsExpr (EAsPat        {})  = panic "dsExpr:EAsPat"
-dsExpr (EViewPat      {})  = panic "dsExpr:EViewPat"
-dsExpr (ELazyPat      {})  = panic "dsExpr:ELazyPat"
-dsExpr (HsAppType     {})  = panic "dsExpr:HsAppType" -- removed by typechecker
-dsExpr (HsDo          {})  = panic "dsExpr:HsDo"
-dsExpr (HsRecFld      {})  = panic "dsExpr:HsRecFld"
+ds_expr _ (ExprWithTySig {})  = panic "dsExpr:ExprWithTySig"
+ds_expr _ (HsBracket     {})  = panic "dsExpr:HsBracket"
+ds_expr _ (HsArrApp      {})  = panic "dsExpr:HsArrApp"
+ds_expr _ (HsArrForm     {})  = panic "dsExpr:HsArrForm"
+ds_expr _ (EWildPat      {})  = panic "dsExpr:EWildPat"
+ds_expr _ (EAsPat        {})  = panic "dsExpr:EAsPat"
+ds_expr _ (EViewPat      {})  = panic "dsExpr:EViewPat"
+ds_expr _ (ELazyPat      {})  = panic "dsExpr:ELazyPat"
+ds_expr _ (HsAppType     {})  = panic "dsExpr:HsAppType" -- removed by typechecker
+ds_expr _ (HsDo          {})  = panic "dsExpr:HsDo"
+ds_expr _ (HsRecFld      {})  = panic "dsExpr:HsRecFld"
 
 ------------------------------
 dsSyntaxExpr :: SyntaxExpr Id -> [CoreExpr] -> DsM CoreExpr
@@ -1007,14 +1013,31 @@ mk_fail_msg dflags pat = "Pattern match failure in do expression at " ++
 {-
 ************************************************************************
 *                                                                      *
-   Desugaring ConLikes
+   Desugaring Variables
 *                                                                      *
 ************************************************************************
 -}
 
-dsConLike :: ConLike -> CoreExpr
-dsConLike (RealDataCon dc) = Var (dataConWrapId dc)
-dsConLike (PatSynCon ps) = case patSynBuilder ps of
+dsHsVar :: Bool  -- are we directly inside an HsWrap?
+                 -- See Wrinkle in Note [Detecting forced eta expansion]
+        -> Id -> DsM CoreExpr
+dsHsVar w var
+  | not w
+  , let bad_tys = badUseOfLevPolyPrimop var ty
+  , not (null bad_tys)
+  = do { levPolyPrimopErr var ty bad_tys
+       ; return unitExpr }  -- return something eminently safe
+
+  | otherwise
+  = return (varToCoreExpr var)   -- See Note [Desugaring vars]
+
+  where
+    ty = idType var
+
+dsConLike :: Bool  -- as in dsHsVar
+          -> ConLike -> DsM CoreExpr
+dsConLike w (RealDataCon dc) = dsHsVar w (dataConWrapId dc)
+dsConLike _ (PatSynCon ps)   = return $ case patSynBuilder ps of
   Just (id, add_void)
     | add_void  -> mkCoreApp (text "dsConLike" <+> ppr ps) (Var id) (Var voidPrimId)
     | otherwise -> Var id
@@ -1064,3 +1087,90 @@ badMonadBind rhs elt_ty
          , hang (text "Suppress this warning by saying")
               2 (quotes $ text "_ <-" <+> ppr rhs)
          ]
+
+{-
+************************************************************************
+*                                                                      *
+   Forced eta expansion and levity polymorphism
+*                                                                      *
+************************************************************************
+
+Note [Detecting forced eta expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We cannot have levity polymorphic function arguments. See
+Note [Levity polymorphism invariants] in CoreSyn. But we *can* have
+functions that take levity polymorphism arguments, as long as these
+functions are eta-reduced. (See #12708 for an example.)
+
+However, we absolutely cannot do this for functions that have no
+binding (i.e., say True to Id.hasNoBinding), like primops and unboxed
+tuple constructors. These get eta-expanded in CorePrep.maybeSaturate.
+
+Detecting when this is about to happen is a bit tricky, though. When
+the desugarer is looking at the Id itself (let's be concrete and
+suppose we have (#,#)), we don't know whether it will be levity
+polymorphic. So the right spot seems to be to look after the Id has
+been applied to its type arguments. To make the algorithm efficient,
+it's important to be able to spot ((#,#) @a @b @c @d) without looking
+past all the type arguments. We thus require that
+  * The body of an HsWrap is not an HsWrap.
+With that representation invariant, we simply look inside every HsWrap
+to see if its body is an HsVar whose Id hasNoBinding. Then, we look
+at the wrapped type. If it has any levity polymorphic arguments, reject.
+
+Interestingly, this approach does not look to see whether the Id in
+question will be eta expanded. The logic is this:
+  * Either the Id in question is saturated or not.
+  * If it is, then it surely can't have levity polymorphic arguments.
+    If its wrapped type contains levity polymorphic arguments, reject.
+  * If it's not, then it can't be eta expanded with levity polymorphic
+    argument. If its wrapped type contains levity polymorphic arguments, reject.
+So, either way, we're good to reject.
+
+Wrinkle
+~~~~~~~
+Not all polymorphic Ids are wrapped in
+HsWrap, due to the lazy instantiation of TypeApplications. (See "Visible type
+application", ESOP '16.) But if we spot a levity-polymorphic hasNoBinding Id
+without a wrapper, then that is surely problem and we can reject.
+
+We thus have a parameter to `dsExpr` that tracks whether or not we are
+directly in an HsWrap. If we find a levity-polymorphic hasNoBinding Id when
+we're not directly in an HsWrap, reject.
+
+-}
+
+-- | Takes an expression and its instantiated type. If the expression is an
+-- HsVar with a hasNoBinding primop and the type has levity-polymorphic arguments,
+-- issue an error. See Note [Detecting forced eta expansion]
+checkForcedEtaExpansion :: HsExpr Id -> Type -> DsM ()
+checkForcedEtaExpansion expr ty
+  | Just var <- case expr of
+                  HsVar (L _ var)               -> Just var
+                  HsConLikeOut (RealDataCon dc) -> Just (dataConWrapId dc)
+                  _                             -> Nothing
+  , let bad_tys = badUseOfLevPolyPrimop var ty
+  , not (null bad_tys)
+  = levPolyPrimopErr var ty bad_tys
+checkForcedEtaExpansion _ _ = return ()
+
+-- | Is this a hasNoBinding Id with a levity-polymorphic type?
+-- Returns the arguments that are levity polymorphic if they are bad;
+-- or an empty list otherwise
+-- See Note [Detecting forced eta expansion]
+badUseOfLevPolyPrimop :: Id -> Type -> [Type]
+badUseOfLevPolyPrimop id ty
+  | hasNoBinding id
+  = filter isTypeLevPoly arg_tys
+  | otherwise
+  = []
+  where
+    (binders, _) = splitPiTys ty
+    arg_tys      = mapMaybe binderRelevantType_maybe binders
+
+levPolyPrimopErr :: Id -> Type -> [Type] -> DsM ()
+levPolyPrimopErr primop ty bad_tys
+  = errDs $ vcat [ hang (text "Cannot use primitive with levity-polymorphic arguments:")
+                      2 (ppr primop <+> dcolon <+> ppr ty)
+                 , hang (text "Levity-polymorphic arguments:")
+                      2 (vcat (map (\t -> ppr t <+> dcolon <+> ppr (typeKind t)) bad_tys)) ]
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index fdca76c5b8..8345859d92 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -289,8 +289,7 @@ it easier to read debugging output.
 
 Note [Levity polymorphism checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-According to the Levity Polymorphism paper
-<http://cs.brynmawr.edu/~rae/papers/2017/levity/levity.pdf>, levity
+According to the "Levity Polymorphism" paper (PLDI '17), levity
 polymorphism is forbidden in precisely two places: in the type of a bound
 term-level argument and in the type of an argument to a function. The paper
 explains it more fully, but briefly: expressions in these contexts need to be
diff --git a/compiler/hsSyn/HsExpr.hs b/compiler/hsSyn/HsExpr.hs
index f3cc3d0861..64e2ffef73 100644
--- a/compiler/hsSyn/HsExpr.hs
+++ b/compiler/hsSyn/HsExpr.hs
@@ -689,6 +689,9 @@ data HsExpr id
 
   ---------------------------------------
   -- Finally, HsWrap appears only in typechecker output
+  -- The contained Expr is *NOT* itself an HsWrap.
+  -- See Note [Detecting forced eta expansion] in DsExpr. This invariant
+  -- is maintained by HsUtils.mkHsWrap.
 
   |  HsWrap     HsWrapper    -- TRANSLATION
                 (HsExpr id)
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index c7d43b02a1..1be9055402 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -196,7 +196,7 @@ mkHsCaseAlt pat expr
   = mkSimpleMatch CaseAlt [pat] expr
 
 nlHsTyApp :: name -> [Type] -> LHsExpr name
-nlHsTyApp fun_id tys = noLoc (HsWrap (mkWpTyApps tys) (HsVar (noLoc fun_id)))
+nlHsTyApp fun_id tys = noLoc (mkHsWrap (mkWpTyApps tys) (HsVar (noLoc fun_id)))
 
 nlHsTyApps :: name -> [Type] -> [LHsExpr name] -> LHsExpr name
 nlHsTyApps fun_id tys xs = foldl nlHsApp (nlHsTyApp fun_id tys) xs
@@ -654,9 +654,12 @@ typeToLHsType ty
 mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
 mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
 
+-- Avoid (HsWrap co (HsWrap co' _)).
+-- See Note [Detecting forced eta expansion] in DsExpr
 mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
 mkHsWrap co_fn e | isIdHsWrapper co_fn = e
-                 | otherwise           = HsWrap co_fn e
+mkHsWrap co_fn (HsWrap co_fn' e)       = mkHsWrap (co_fn <.> co_fn') e
+mkHsWrap co_fn e                       = HsWrap co_fn e
 
 mkHsWrapCo :: TcCoercionN   -- A Nominal coercion  a ~N b
            -> HsExpr id -> HsExpr id
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index f3874ab1dc..70e444e65c 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -371,7 +371,7 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
 
     -- Coerces a `t` into a dictionry for `IP "x" t`.
     -- co : t -> IP "x" t
-    toDict ipClass x ty = HsWrap $ mkWpCastR $
+    toDict ipClass x ty = mkHsWrap $ mkWpCastR $
                           wrapIP $ mkClassPred ipClass [x,ty]
 
 {- Note [Implicit parameter untouchables]
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index e521b735a4..7f7f734ca9 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -211,7 +211,7 @@ tcExpr e@(HsIPVar x) res_ty
                       ip_ty res_ty }
   where
   -- Coerces a dictionary for `IP "x" t` into `t`.
-  fromDict ipClass x ty = HsWrap $ mkWpCastR $
+  fromDict ipClass x ty = mkHsWrap $ mkWpCastR $
                           unwrapIP $ mkClassPred ipClass [x,ty]
   origin = IPOccOrigin x
 
@@ -230,7 +230,7 @@ tcExpr e@(HsOverLabel mb_fromLabel l) res_ty
   where
   -- Coerces a dictionary for `IsLabel "x" t` into `t`,
   -- or `HasField "x" r a into `r -> a`.
-  fromDict pred = HsWrap $ mkWpCastR $ unwrapIP pred
+  fromDict pred = mkHsWrap $ mkWpCastR $ unwrapIP pred
   origin = OverLabelOrigin l
   lbl = mkStrLitTy l
 
@@ -354,8 +354,8 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
                   tc_poly_expr_nc arg2 arg2_exp_ty
        ; arg2_ty <- readExpType arg2_exp_ty
        ; op_id <- tcLookupId op_name
-       ; let op' = L loc (HsWrap (mkWpTyApps [arg1_ty, arg2_ty])
-                                 (HsVar (L lv op_id)))
+       ; let op' = L loc (mkHsWrap (mkWpTyApps [arg1_ty, arg2_ty])
+                                   (HsVar (L lv op_id)))
        ; return $ OpApp arg1' op' fix arg2' }
 
   | (L loc (HsVar (L lv op_name))) <- op
@@ -392,10 +392,10 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
 
        ; op_id  <- tcLookupId op_name
        ; res_ty <- readExpType res_ty
-       ; let op' = L loc (HsWrap (mkWpTyApps [ getRuntimeRep "tcExpr ($)" res_ty
-                                             , arg2_sigma
-                                             , res_ty])
-                                 (HsVar (L lv op_id)))
+       ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep "tcExpr ($)" res_ty
+                                               , arg2_sigma
+                                               , res_ty])
+                                   (HsVar (L lv op_id)))
              -- arg1' :: arg1_ty
              -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
              -- wrap_res :: op_res_ty "->" res_ty
@@ -1793,7 +1793,7 @@ tcSeq loc fun_name args res_ty
         ; arg1' <- tcMonoExpr arg1 (mkCheckExpType arg1_ty)
         ; arg2' <- tcMonoExpr arg2 arg2_exp_ty
         ; res_ty <- readExpType res_ty  -- by now, it's surely filled in
-        ; let fun'    = L loc (HsWrap ty_args (HsVar (L loc fun)))
+        ; let fun'    = L loc (mkHsWrap ty_args (HsVar (L loc fun)))
               ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
         ; return (idHsWrapper, fun', [Left arg1', Left arg2']) }
 
@@ -1835,7 +1835,7 @@ tcTagToEnum loc fun_name args res_ty
                  (mk_error ty' doc2)
 
        ; arg' <- tcMonoExpr arg (mkCheckExpType intPrimTy)
-       ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
+       ; let fun' = L loc (mkHsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
              rep_ty = mkTyConApp rep_tc rep_args
 
        ; return (mkWpCastR (mkTcSymCo coi), fun', [Left arg']) }
diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs
index e7deedee15..909314e519 100644
--- a/compiler/typecheck/TcMatches.hs
+++ b/compiler/typecheck/TcMatches.hs
@@ -507,7 +507,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
                              poly_arg_ty `mkFunTy` poly_res_ty
 
        ; using' <- tcPolyExpr using using_poly_ty
-       ; let final_using = fmap (HsWrap (WpTyApp tup_ty)) using'
+       ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
 
              -- 'stmts' returns a result of type (m1_ty tuple_ty),
              -- typically something like [(Int,Bool,Int)]
@@ -689,7 +689,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
        -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c))
 
        ; using' <- tcPolyExpr using using_poly_ty
-       ; let final_using = fmap (HsWrap (WpTyApp tup_ty)) using'
+       ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
 
        --------------- Bulding the bindersMap ----------------
        ; let mk_n_bndr :: Name -> TcId -> TcId
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 1e4ec4060b..b90de5e459 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -574,8 +574,8 @@ runAnnotation target expr = do
                 -- and hence ensures the appropriate dictionary is bound by const_binds
               ; wrapper <- instCall AnnOrigin [expr_ty] [mkClassPred data_class [expr_ty]]
               ; let specialised_to_annotation_wrapper_expr
-                      = L loc (HsWrap wrapper
-                                      (HsVar (L loc to_annotation_wrapper_id)))
+                      = L loc (mkHsWrap wrapper
+                                        (HsVar (L loc to_annotation_wrapper_id)))
               ; return (L loc (HsApp specialised_to_annotation_wrapper_expr expr')) }
 
     -- Run the appropriately wrapped expression to get the value of
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index 906c6978bd..ae11c8a651 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -11,7 +11,6 @@ module Kind (
         isTYPEApp,
         returnsTyCon, returnsConstraintKind,
         isConstraintKindCon,
-        okArrowArgKind, okArrowResultKind,
 
         classifiesTypeWithValues,
         isStarKind, isStarKindSynonymTyCon,
@@ -116,17 +115,6 @@ isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
       = False
 
 
---------------------------------------------
---            Kinding for arrow (->)
--- Says when a kind is acceptable on lhs or rhs of an arrow
---     arg -> res
---
--- See Note [Levity polymorphism]
-
-okArrowArgKind, okArrowResultKind :: Kind -> Bool
-okArrowArgKind    = classifiesTypeWithValues
-okArrowResultKind = classifiesTypeWithValues
-
 -----------------------------------------
 --              Subkinding
 -- The tc variants are used during type-checking, where ConstraintKind
@@ -162,31 +150,3 @@ isStarKind _ = False
 -- | Is the tycon @Constraint@?
 isStarKindSynonymTyCon :: TyCon -> Bool
 isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey
-
-
-{- Note [Levity polymorphism]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Is this type legal?
-   (a :: TYPE rep) -> Int
-   where 'rep :: RuntimeRep'
-
-You might think not, because no lambda can have a
-runtime-rep-polymorphic binder.  So no lambda has the
-above type.  BUT here's a way it can be useful (taken from
-Trac #12708):
-
-  data T rep (a :: TYPE rep)
-     = MkT (a -> Int)
-
-  x1 :: T LiftedRep Int
-  x1 =  MkT LiftedRep Int  (\x::Int -> 3)
-
-  x2 :: T IntRep Int#
-  x2 = MkT IntRep Int# (\x:Int# -> 3)
-
-Note that the lambdas are just fine!
-
-Hence, okArrowArgKind and okArrowResultKind both just
-check that the type is of the form (TYPE r) for some
-representation type r.
--}
diff --git a/testsuite/tests/codeGen/should_compile/T13233.hs b/testsuite/tests/codeGen/should_compile/T13233.hs
deleted file mode 100644
index bb79856d3b..0000000000
--- a/testsuite/tests/codeGen/should_compile/T13233.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE UnboxedTuples #-}
-module Bug where
-
-import GHC.Exts (TYPE)
-
-class Foo (a :: TYPE rep) where
-  bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
-
-baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
-baz = bar (#,#)
diff --git a/testsuite/tests/codeGen/should_compile/all.T b/testsuite/tests/codeGen/should_compile/all.T
index a73a9d65cf..6ae4e1cb4e 100644
--- a/testsuite/tests/codeGen/should_compile/all.T
+++ b/testsuite/tests/codeGen/should_compile/all.T
@@ -35,4 +35,3 @@ test('T10667', [ when((arch('powerpc64') or arch('powerpc64le')),
      compile, ['-g'])
 test('T12115', normal, compile, [''])
 test('T12355', normal, compile, [''])
-test('T13233', expect_broken(13233), compile, [''])
diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs
new file mode 100644
index 0000000000..fa5a37b046
--- /dev/null
+++ b/testsuite/tests/codeGen/should_fail/T13233.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MagicHash #-}
+module Bug where
+
+import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
+
+class Foo (a :: TYPE rep) where
+  bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+
+baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz = bar (#,#)
+
+obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
+                   (a :: TYPE rep1) (b :: TYPE rep2).
+                   a -> b -> (# a, b #)) -> ()
+obscure _ = ()
+
+quux :: ()
+quux = obscure (#,#)
+
+primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
+          a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
+       -> State# RealWorld -> (# State# RealWorld, Weak# b #)
+primop = mkWeak#
diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr
new file mode 100644
index 0000000000..2d167cf5f7
--- /dev/null
+++ b/testsuite/tests/codeGen/should_fail/T13233.stderr
@@ -0,0 +1,24 @@
+
+T13233.hs:14:11: error:
+    Cannot use primitive with levity-polymorphic arguments:
+      GHC.Prim.(#,#) :: a -> a -> (# a, a #)
+    Levity polymorphic arguments:
+      a :: TYPE rep
+      a :: TYPE rep
+
+T13233.hs:22:16: error:
+    Cannot use primitive with levity-polymorphic arguments:
+      GHC.Prim.(#,#) :: forall (a :: TYPE rep1) (b :: TYPE rep2).
+                        a -> b -> (# a, b #)
+    Levity polymorphic arguments:
+      a :: TYPE rep1
+      b :: TYPE rep2
+
+T13233.hs:27:10: error:
+    Cannot use primitive with levity-polymorphic arguments:
+      mkWeak# :: a
+                 -> b
+                 -> (State# RealWorld -> (# State# RealWorld, c #))
+                 -> State# RealWorld
+                 -> (# State# RealWorld, Weak# b #)
+    Levity polymorphic arguments: a :: TYPE rep
diff --git a/testsuite/tests/codeGen/should_fail/all.T b/testsuite/tests/codeGen/should_fail/all.T
index 7e25b5f693..1fe2141caf 100644
--- a/testsuite/tests/codeGen/should_fail/all.T
+++ b/testsuite/tests/codeGen/should_fail/all.T
@@ -3,3 +3,4 @@
 # Only the LLVM code generator consistently forces the alignment of
 # memcpy operations
 test('T8131', [cmm_src, only_ways(llvm_ways)], compile_fail, [''])
+test('T13233', normal, compile_fail, [''])