Visible type application

This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

1 files changed, 13 insertions, 1 deletions

diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index f5d5ed553b..7ce60bc852 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -972,14 +972,26 @@ getErrCtxt = do { env <- getLclEnv; return (tcl_ctxt env) }
 setErrCtxt :: [ErrCtxt] -> TcM a -> TcM a
 setErrCtxt ctxt = updLclEnv (\ env -> env { tcl_ctxt = ctxt })
 
+-- | Add a fixed message to the error context. This message should not
+-- do any tidying.
 addErrCtxt :: MsgDoc -> TcM a -> TcM a
 addErrCtxt msg = addErrCtxtM (\env -> return (env, msg))
 
+-- | Add a message to the error context. This message may do tidying.
 addErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
 addErrCtxtM ctxt = updCtxt (\ ctxts -> (False, ctxt) : ctxts)
 
+-- | Add a fixed landmark message to the error context. A landmark
+-- message is always sure to be reported, even if there is a lot of
+-- context. It also doesn't count toward the maximum number of contexts
+-- reported.
 addLandmarkErrCtxt :: MsgDoc -> TcM a -> TcM a
-addLandmarkErrCtxt msg = updCtxt (\ctxts -> (True, \env -> return (env,msg)) : ctxts)
+addLandmarkErrCtxt msg = addLandmarkErrCtxtM (\env -> return (env, msg))
+
+-- | Variant of 'addLandmarkErrCtxt' that allows for monadic operations
+-- and tidying.
+addLandmarkErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
+addLandmarkErrCtxtM ctxt = updCtxt (\ctxts -> (True, ctxt) : ctxts)
 
 -- Helper function for the above
 updCtxt :: ([ErrCtxt] -> [ErrCtxt]) -> TcM a -> TcM a