Update levity polymorphism

This commit implements the proposal in
https://github.com/ghc-proposals/ghc-proposals/pull/29 and
https://github.com/ghc-proposals/ghc-proposals/pull/35.

Here are some of the pieces of that proposal:

* Some of RuntimeRep's constructors have been shortened.

* TupleRep and SumRep are now parameterized over a list of RuntimeReps.
* This
means that two types with the same kind surely have the same
representation.
Previously, all unboxed tuples had the same kind, and thus the fact
above was
false.

* RepType.typePrimRep and friends now return a *list* of PrimReps. These
functions can now work successfully on unboxed tuples. This change is
necessary because we allow abstraction over unboxed tuple types and so
cannot
always handle unboxed tuples specially as we did before.

* We sometimes have to create an Id from a PrimRep. I thus split PtrRep
* into
LiftedRep and UnliftedRep, so that the created Ids have the right
strictness.

* The RepType.RepType type was removed, as it didn't seem to help with
* much.

* The RepType.repType function is also removed, in favor of typePrimRep.

* I have waffled a good deal on whether or not to keep VoidRep in
TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
represented in RuntimeRep, and typePrimRep will never return a list
including
VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
imagine another design choice where we have a PrimRepV type that is
PrimRep
with an extra constructor. That seemed to be a heavier design, though,
and I'm
not sure what the benefit would be.

* The last, unused vestiges of # (unliftedTypeKind) have been removed.

* There were several pretty-printing bugs that this change exposed;
* these are fixed.

* We previously checked for levity polymorphism in the types of binders.
* But we
also must exclude levity polymorphism in function arguments. This is
hard to check
for, requiring a good deal of care in the desugarer. See Note [Levity
polymorphism
checking] in DsMonad.

* In order to efficiently check for levity polymorphism in functions, it
* was necessary
to add a new bit of IdInfo. See Note [Levity info] in IdInfo.

* It is now safe for unlifted types to be unsaturated in Core. Core Lint
* is updated
accordingly.

* We can only know strictness after zonking, so several checks around
* strictness
in the type-checker (checkStrictBinds, the check for unlifted variables
under a ~
pattern) have been moved to the desugarer.

* Along the way, I improved the treatment of unlifted vs. banged
* bindings. See
Note [Strict binds checks] in DsBinds and #13075.

* Now that we print type-checked source, we must be careful to print
* ConLikes correctly.
This is facilitated by a new HsConLikeOut constructor to HsExpr.
Particularly troublesome
are unlifted pattern synonyms that get an extra void# argument.

* Includes a submodule update for haddock, getting rid of #.

* New testcases:
  typecheck/should_fail/StrictBinds
  typecheck/should_fail/T12973
  typecheck/should_run/StrictPats
  typecheck/should_run/T12809
  typecheck/should_fail/T13105
  patsyn/should_fail/UnliftedPSBind
  typecheck/should_fail/LevPolyBounded
  typecheck/should_compile/T12987
  typecheck/should_compile/T11736

* Fixed tickets:
  #12809
  #12973
  #11736
  #13075
  #12987

* This also adds a test case for #13105. This test case is
* "compile_fail" and
succeeds, because I want the testsuite to monitor the error message.
When #13105 is fixed, the test case will compile cleanly.

1 files changed, 125 insertions, 13 deletions

diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index d46aeaab7a..24cca5d8b2 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -12,10 +12,11 @@
 module DsMonad (
         DsM, mapM, mapAndUnzipM,
         initDs, initDsTc, initTcDsForSolver, fixDs,
-        foldlM, foldrM, whenGOptM, unsetGOptM, unsetWOptM,
+        foldlM, foldrM, whenGOptM, unsetGOptM, unsetWOptM, xoptM,
         Applicative(..),(<$>),
 
-        duplicateLocalDs, newSysLocalDs, newSysLocalsDs, newUniqueId,
+        duplicateLocalDs, newSysLocalDsNoLP, newSysLocalDs,
+        newSysLocalsDsNoLP, newSysLocalsDs, newUniqueId,
         newFailLocalDs, newPredVarDs,
         getSrcSpanDs, putSrcSpanDs,
         mkPrintUnqualifiedDs,
@@ -36,20 +37,28 @@ module DsMonad (
         -- Iterations for pm checking
         incrCheckPmIterDs, resetPmIterDs,
 
-        -- Warnings
-        DsWarning, warnDs, failWithDs, discardWarningsDs,
+        -- Warnings and errors
+        DsWarning, warnDs, warnIfSetDs, errDs, errDsCoreExpr,
+        failWithDs, failDs, discardWarningsDs,
+        askNoErrsDs,
 
         -- Data types
         DsMatchContext(..),
         EquationInfo(..), MatchResult(..), DsWrapper, idDsWrapper,
-        CanItFail(..), orFail
+        CanItFail(..), orFail,
+
+        -- Levity polymorphism
+        dsNoLevPoly, dsNoLevPolyExpr
     ) where
 
 import TcRnMonad
 import FamInstEnv
 import CoreSyn
+import MkCore    ( mkCoreTup )
+import CoreUtils ( exprType, isExprLevPoly )
 import HsSyn
 import TcIface
+import TcMType ( checkForLevPolyX, formatLevPolyErr )
 import LoadIface
 import Finder
 import PrelNames
@@ -312,11 +321,51 @@ And all this mysterious stuff is so we can occasionally reach out and
 grab one or more names.  @newLocalDs@ isn't exported---exported
 functions are defined with it.  The difference in name-strings makes
 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
+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
+stored in registers, and it's hard (read, impossible) to store something
+that's levity polymorphic.
+
+We cannot check for bad levity polymorphism conveniently in the type checker,
+because we can't tell, a priori, which levity metavariables will be solved.
+At one point, I (Richard) thought we could check in the zonker, but it's hard
+to know where precisely are the abstracted variables and the arguments. So
+we check in the desugarer, the only place where we can see the Core code and
+still report respectable syntax to the user. This covers the vast majority
+of cases; see calls to DsMonad.dsNoLevPoly and friends.
+
+Levity polymorphism is also prohibited in the types of binders, and the
+desugarer checks for this in GHC-generated Ids. (The zonker handles
+the user-writted ids in zonkIdBndr.) This is done in newSysLocalDsNoLP.
+The newSysLocalDs variant is used in the vast majority of cases where
+the binder is obviously not levity polymorphic, omitting the check.
+It would be nice to ASSERT that there is no levity polymorphism here,
+but we can't, because of the fixM in DsArrows. It's all OK, though:
+Core Lint will catch an error here.
+
+However, the desugarer is the wrong place for certain checks. In particular,
+the desugarer can't report a sensible error message if an HsWrapper is malformed.
+After all, GHC itself produced the HsWrapper. So we store some message text
+in the appropriate HsWrappers (e.g. WpFun) that we can print out in the
+desugarer.
+
+There are a few more checks in places where Core is generated outside the
+desugarer. For example, in datatype and class declarations, where levity
+polymorphism is checked for during validity checking. It would be nice to
+have one central place for all this, but that doesn't seem possible while
+still reporting nice error messages.
+
 -}
 
 -- Make a new Id with the same print name, but different type, and new unique
 newUniqueId :: Id -> Type -> DsM Id
-newUniqueId id = mkSysLocalOrCoVarM (occNameFS (nameOccName (idName id)))
+newUniqueId id = mk_local (occNameFS (nameOccName (idName id)))
 
 duplicateLocalDs :: Id -> DsM Id
 duplicateLocalDs old_local
@@ -327,12 +376,26 @@ newPredVarDs :: PredType -> DsM Var
 newPredVarDs pred
  = newSysLocalDs pred
 
-newSysLocalDs, newFailLocalDs :: Type -> DsM Id
-newSysLocalDs  = mkSysLocalOrCoVarM (fsLit "ds")
+newSysLocalDsNoLP, newSysLocalDs, newFailLocalDs :: Type -> DsM Id
+newSysLocalDsNoLP  = mk_local (fsLit "ds")
+
+-- this variant should be used when the caller can be sure that the variable type
+-- is not levity-polymorphic. It is necessary when the type is knot-tied because
+-- of the fixM used in DsArrows. See Note [Levity polymorphism checking]
+newSysLocalDs = mkSysLocalOrCoVarM (fsLit "ds")
 newFailLocalDs = mkSysLocalOrCoVarM (fsLit "fail")
+  -- the fail variable is used only in a situation where we can tell that
+  -- levity-polymorphism is impossible.
 
-newSysLocalsDs :: [Type] -> DsM [Id]
-newSysLocalsDs tys = mapM newSysLocalDs tys
+newSysLocalsDsNoLP, newSysLocalsDs :: [Type] -> DsM [Id]
+newSysLocalsDsNoLP = mapM newSysLocalDsNoLP
+newSysLocalsDs = mapM newSysLocalDs
+
+mk_local :: FastString -> Type -> DsM Id
+mk_local fs ty = do { dsNoLevPoly ty (text "When trying to create a variable of type:" <+>
+                                      ppr ty)  -- could improve the msg with another
+                                               -- parameter indicating context
+                    ; mkSysLocalOrCoVarM fs ty }
 
 {-
 We can also reach out and either set/grab location information from
@@ -387,6 +450,7 @@ putSrcSpanDs (RealSrcSpan real_span) thing_inside
   = updLclEnv (\ env -> env {dsl_loc = real_span}) thing_inside
 
 -- | Emit a warning for the current source location
+-- NB: Warns whether or not -Wxyz is set
 warnDs :: WarnReason -> SDoc -> DsM ()
 warnDs reason warn
   = do { env <- getGblEnv
@@ -396,15 +460,50 @@ warnDs reason warn
                    mkWarnMsg dflags loc (ds_unqual env) warn
        ; updMutVar (ds_msgs env) (\ (w,e) -> (w `snocBag` msg, e)) }
 
-failWithDs :: SDoc -> DsM a
-failWithDs err
+-- | Emit a warning only if the correct WarnReason is set in the DynFlags
+warnIfSetDs :: WarningFlag -> SDoc -> DsM ()
+warnIfSetDs flag warn
+  = whenWOptM flag $
+    warnDs (Reason flag) warn
+
+errDs :: SDoc -> DsM ()
+errDs err
   = do  { env <- getGblEnv
         ; loc <- getSrcSpanDs
         ; dflags <- getDynFlags
         ; let msg = mkErrMsg dflags loc (ds_unqual env) err
-        ; updMutVar (ds_msgs env) (\ (w,e) -> (w, e `snocBag` msg))
+        ; updMutVar (ds_msgs env) (\ (w,e) -> (w, e `snocBag` msg)) }
+
+-- | Issue an error, but return the expression for (), so that we can continue
+-- reporting errors.
+errDsCoreExpr :: SDoc -> DsM CoreExpr
+errDsCoreExpr err
+  = do { errDs err
+       ; return $ mkCoreTup [] }
+
+failWithDs :: SDoc -> DsM a
+failWithDs err
+  = do  { errDs err
         ; failM }
 
+failDs :: DsM a
+failDs = failM
+
+-- (askNoErrsDs m) runs m
+-- If m fails, (askNoErrsDs m) fails
+-- If m succeeds with result r, (askNoErrsDs m) succeeds with result (r, b),
+--  where b is True iff m generated no errors
+-- Regardless of success or failure, any errors generated by m are propagated
+-- c.f. TcRnMonad.askNoErrs
+askNoErrsDs :: DsM a -> DsM (a, Bool)
+askNoErrsDs m
+ = do { errs_var <- newMutVar emptyMessages
+      ; env <- getGblEnv
+      ; res <- setGblEnv (env { ds_msgs = errs_var }) m
+      ; (warns, errs) <- readMutVar errs_var
+      ; updMutVar (ds_msgs env) (\ (w,e) -> (w `unionBags` warns, e `unionBags` errs))
+      ; return (res, isEmptyBag errs) }
+
 mkPrintUnqualifiedDs :: DsM PrintUnqualified
 mkPrintUnqualifiedDs = ds_unqual <$> getGblEnv
 
@@ -529,3 +628,16 @@ discardWarningsDs thing_inside
         ; writeTcRef (ds_msgs env) old_msgs
 
         ; return result }
+
+-- | Fail with an error message if the type is levity polymorphic.
+dsNoLevPoly :: Type -> SDoc -> DsM ()
+-- See Note [Levity polymorphism checking]
+dsNoLevPoly ty doc = checkForLevPolyX errDs doc ty
+
+-- | Check an expression for levity polymorphism, failing if it is
+-- levity polymorphic.
+dsNoLevPolyExpr :: CoreExpr -> SDoc -> DsM ()
+-- See Note [Levity polymorphism checking]
+dsNoLevPolyExpr e doc
+  | isExprLevPoly e = errDs (formatLevPolyErr (exprType e) $$ doc)
+  | otherwise       = return ()