Remove answers from sent challenges

Also fix integration test

8 files changed, 197 insertions, 190 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/API.hs b/lambda-calcul/haskell/src/Minilang/API.hs
index 0be70ff..9638da8 100644
--- a/lambda-calcul/haskell/src/Minilang/API.hs
+++ b/lambda-calcul/haskell/src/Minilang/API.hs
@@ -17,25 +17,25 @@ import Data.Data (Proxy (..))
 import Data.Text (Text)
 import Data.Time (UTCTime)
 import GHC.Generics (Generic)
-import Servant
-  ( Delete,
-    Description,
-    FromHttpApiData,
-    Get,
-    JSON,
-    Post,
-    QueryParam,
-    Raw,
-    ReqBody,
-    StdMethod (POST),
-    Summary,
-    ToHttpApiData,
-    Verb,
-    parseUrlPiece,
-    toUrlPiece,
-    (:<|>),
-    (:>),
-  )
+import Servant (
+  Delete,
+  Description,
+  FromHttpApiData,
+  Get,
+  JSON,
+  Post,
+  QueryParam,
+  Raw,
+  ReqBody,
+  StdMethod (POST),
+  Summary,
+  ToHttpApiData,
+  Verb,
+  parseUrlPiece,
+  toUrlPiece,
+  (:<|>),
+  (:>),
+ )
 import System.Random (StdGen, uniformList)
 
 type LambdaAPI =
@@ -91,12 +91,13 @@ type GetNextChallenge =
 
 type PostAnswer =
   Summary
-    "Post an answer to the current challenge for the given user." :>
-    Description "The answer should be given as JSON string representing the result \
-    \of evaluating the current challenge's expression in the untyped λ-calculus. This \
-    \textual representation should be consistent with the grammar given in the REPL's \
-    \\"Help\" panel. Expect to be surprised 🤔 !\
-    \"
+    "Post an answer to the current challenge for the given user."
+    :> Description
+         "The answer should be given as JSON string representing the result \
+         \of evaluating the current challenge's expression in the untyped λ-calculus. This \
+         \textual representation should be consistent with the grammar given in the REPL's \
+         \\"Help\" panel. Expect to be surprised 🤔 !\
+         \"
     :> "api"
     :> "challenge"
     :> QueryParam "token" Token
@@ -107,10 +108,10 @@ lambdaAPI :: Proxy LambdaAPI
 lambdaAPI = Proxy
 
 data Score = Score
-  { user :: User,
-    grade :: Int,
-    lastTest :: Maybe UTCTime,
-    lastResult :: Maybe Bool
+  { user :: User
+  , grade :: Int
+  , lastTest :: Maybe UTCTime
+  , lastResult :: Maybe Bool
   }
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
@@ -130,16 +131,15 @@ newToken :: StdGen -> (ByteString, StdGen)
 newToken = first LBS.pack . uniformList 16
 
 data Challenge = Challenge
-  { level :: Int,
-    expr :: Text,
-    description :: Text,
-    answer :: Text
+  { level :: Int
+  , expr :: Text
+  , description :: Text
   }
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
 defaultChallenges :: [Challenge]
 defaultChallenges =
-  [ Challenge 0 "x" "A lone free variable. What does x reduce to?" "x",
-    Challenge 1 "y" "Another free variable. What does y reduce to?" "y",
-    Challenge 2 "(lam (x) x)" "The identity function. What is its normal form?" "(lam (x) x)"
+  [ Challenge 0 "x" "A lone free variable. What does x reduce to?"
+  , Challenge 1 "y" "Another free variable. What does y reduce to?"
+  , Challenge 2 "(lam (x) x)" "The identity function. What is its normal form?"
   ]
diff --git a/lambda-calcul/haskell/src/Minilang/App.hs b/lambda-calcul/haskell/src/Minilang/App.hs
index 0174547..4340708 100644
--- a/lambda-calcul/haskell/src/Minilang/App.hs
+++ b/lambda-calcul/haskell/src/Minilang/App.hs
@@ -20,19 +20,19 @@ import Data.Text.Encoding (decodeUtf8, encodeUtf8)
 import Data.Time (getCurrentTime)
 import Minilang.API (Challenge (..), LambdaAPI, Score (..), Token (..), User (..), newToken)
 import Minilang.Lambda.Parser (pretty)
-import Minilang.REPL (withInputs, replEnvWith)
+import Minilang.REPL (replEnvWith, withInputs)
 import Minilang.REPL.Purer (PurerEnv (..))
-import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..), initialREPL)
+import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..))
 import Network.Wai.Application.Static (defaultFileServerSettings, staticApp)
-import Servant (ServerT, err400, err500, errBody, (:<|>) (..), err404)
+import Servant (ServerT, err400, err404, err500, errBody, (:<|>) (..))
 import Servant.Server (Application, Handler (..), Tagged (..))
 import System.Random (StdGen)
 
 data Env = Env
-  { gen :: TVar StdGen,
-    users :: TVar (Map Token Score),
-    challenges :: [Challenge],
-    evaluator :: Evaluator
+  { gen :: TVar StdGen
+  , users :: TVar (Map Token Score)
+  , challenges :: [Challenge]
+  , evaluator :: Evaluator
   }
 
 makeEnv :: StdGen -> [Challenge] -> Evaluator -> IO Env
@@ -72,7 +72,7 @@ registerUser user@(User name) = do
   pure token
 
 unregisterUser :: (MonadReader Env m, MonadIO m) => Maybe Token -> m Score
-unregisterUser Nothing = liftIO $ throwM $ err400 {errBody = "Missing token"}
+unregisterUser Nothing = liftIO $ throwM $ err400{errBody = "Missing token"}
 unregisterUser (Just token) = do
   checkUserToken token
   score <-
@@ -84,7 +84,7 @@ unregisterUser (Just token) = do
         writeTVar tvar updatedMap
         pure score
   case score of
-    Nothing -> liftIO $ throwM $ err400 {errBody = "User does not exist"}
+    Nothing -> liftIO $ throwM $ err400{errBody = "User does not exist"}
     Just s -> pure s
 
 checkDuplicateUser :: (MonadIO m, MonadReader Env m) => Text -> m ()
@@ -93,10 +93,10 @@ checkDuplicateUser name =
     usersMap <- readTVar user
     when (isUserRegistered name usersMap) $
       throwM $
-        err400 {errBody = "User already registered"}
+        err400{errBody = "User already registered"}
 
 isUserRegistered :: Text -> Map Token Score -> Bool
-isUserRegistered name = Map.foldr (\Score {user = User {username}} acc -> username == name || acc) False
+isUserRegistered name = Map.foldr (\Score{user = User{username}} acc -> username == name || acc) False
 
 generateToken :: (MonadReader Env m, MonadIO m) => m Token
 generateToken =
@@ -116,11 +116,11 @@ getUser :: (MonadIO m, MonadReader Env m) => Maybe Token -> m Score
 getUser mToken = do
   usersMap <- asks users >>= liftIO . readTVarIO
   case mToken >>= (`Map.lookup` usersMap) of
-    Nothing -> liftIO $ throwM $ err404 {errBody = "User does not exist"}
+    Nothing -> liftIO $ throwM $ err404{errBody = "User does not exist"}
     Just score -> pure score
 
 getChallenge :: (MonadReader Env m, MonadIO m) => Maybe Token -> m Challenge
-getChallenge Nothing = liftIO $ throwM $ err400 {errBody = "Missing token"}
+getChallenge Nothing = liftIO $ throwM $ err400{errBody = "Missing token"}
 getChallenge (Just token) = do
   checkUserToken token
   getCurrentChallenge token
@@ -129,7 +129,7 @@ checkUserToken :: (MonadReader Env m, MonadIO m) => Token -> m ()
 checkUserToken token = do
   usersMap <- asks users >>= liftIO . readTVarIO
   case Map.lookup token usersMap of
-    Nothing -> liftIO $ throwM $ err400 {errBody = "Token " <> LBS.fromStrict (encodeUtf8 (unToken token)) <> " does not exist"}
+    Nothing -> liftIO $ throwM $ err400{errBody = "Token " <> LBS.fromStrict (encodeUtf8 (unToken token)) <> " does not exist"}
     Just _ -> pure ()
 
 updateUserLastTest :: (MonadIO m, MonadReader Env m) => Token -> TestResult -> m ()
@@ -138,28 +138,28 @@ updateUserLastTest token result = do
   asks users >>= \user -> liftIO $ atomically $ do
     usersMap <- readTVar user
     case Map.lookup token usersMap of
-      Nothing -> throwM $ err400 {errBody = "Cannot update last test: Invalid token"}
+      Nothing -> throwM $ err400{errBody = "Cannot update last test: Invalid token"}
       Just score -> do
-        let updatedScore = score {lastTest = Just time, lastResult = Just (isSuccess result)}
+        let updatedScore = score{lastTest = Just time, lastResult = Just (isSuccess result)}
             updatedMap = Map.insert token updatedScore usersMap
         writeTVar user updatedMap
 
 postAnswer :: (MonadReader Env m, MonadIO m) => Maybe Token -> Text -> m ()
-postAnswer Nothing _ = liftIO $ throwM $ err400 {errBody = "Missing token"}
-postAnswer (Just token) expected = do
+postAnswer Nothing _ = liftIO $ throwM $ err400{errBody = "Missing token"}
+postAnswer (Just token) answer = do
   checkUserToken token
-  Challenge {expr} <- getCurrentChallenge token
+  Challenge{level, expr} <- getCurrentChallenge token
   ev <- asks evaluator
-  let PurerEnv {outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))]
-      result = evaluateOutputs outputs expected
+  let PurerEnv{outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))]
+      result = evaluateAnswer level outputs answer
   updateUserLastTest token result
   case result of
     TestSucceeded ->
       upgradeUserChallenge token
     TestFailed msg ->
-      liftIO $ throwM $ err400 {errBody = "Test failed: " <> LBS.fromStrict (encodeUtf8 msg)}
+      liftIO $ throwM $ err400{errBody = "Test failed: " <> LBS.fromStrict (encodeUtf8 msg)}
     TestErrored msg ->
-      liftIO $ throwM $ err500 {errBody = "Error evaluating answer: " <> LBS.fromStrict (encodeUtf8 msg)}
+      liftIO $ throwM $ err500{errBody = "Error evaluating answer: " <> LBS.fromStrict (encodeUtf8 msg)}
 
 data TestResult = TestSucceeded | TestFailed Text | TestErrored Text
 
@@ -167,17 +167,17 @@ isSuccess :: TestResult -> Bool
 isSuccess TestSucceeded = True
 isSuccess _ = False
 
-evaluateOutputs :: [Out] -> Text -> TestResult
-evaluateOutputs outputs expected =
+evaluateAnswer :: Int -> [Out] -> Text -> TestResult
+evaluateAnswer grade outputs answer =
   case outputs of
     [Bye, Evaluated ast _ _] ->
-      if pretty ast /= expected
-        then TestFailed "Incorrect result"
+      if pretty ast /= answer
+        then TestFailed $ "Incorrect result for question " <> pack (show grade) <> " got " <> answer <> ", try again"
         else TestSucceeded
     [Bye] ->
-      if expected == ""
+      if answer == ""
         then TestSucceeded
-        else TestFailed "Incorrect result"
+        else TestFailed $ "Incorrect result for question " <> pack (show grade) <> " got " <> answer <> ", try again"
     [Bye, Msg msg] -> TestFailed msg
     _ -> TestErrored $ pack $ show outputs
 
@@ -186,20 +186,20 @@ upgradeUserChallenge token = do
   asks users >>= \user -> liftIO $ atomically $ do
     usersMap <- readTVar user
     case Map.lookup token usersMap of
-      Nothing -> throwM $ err400 {errBody = "Cannot update last test: Invalid token"}
+      Nothing -> throwM $ err400{errBody = "Cannot update last test: Invalid token"}
       Just score -> do
-        let updatedScore = score {grade = succ (grade score)}
+        let updatedScore = score{grade = succ (grade score)}
             updatedMap = Map.insert token updatedScore usersMap
         writeTVar user updatedMap
 
 getCurrentChallenge :: (MonadIO m, MonadReader Env m) => Token -> m Challenge
 getCurrentChallenge token = do
-  Env {users, challenges} <- ask
+  Env{users, challenges} <- ask
   liftIO $ atomically $ do
     usersMap <- readTVar users
     case Map.lookup token usersMap of
-      Nothing -> throwM $ err400 {errBody = "Cannot find challenge: Invalid token"}
-      Just Score {grade} ->
+      Nothing -> throwM $ err400{errBody = "Cannot find challenge: Invalid token"}
+      Just Score{grade} ->
         pure $ challenges !! grade
 
 -- | Serve static resources under `public/` directory
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs
index fbaf35d..82ab8bf 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs
@@ -19,46 +19,46 @@ loadProgram ::
   Env ->
   Context ->
   [AST] ->
-  Either TypeError ([(Term, Type)], Env, Context)
+  Either TypeError ([(Term, Maybe Type)], Env, Context)
 loadProgram evaluator language env context exprs =
   fmap (\(res, e, c) -> (reverse res, e, c)) result
-  where
-    result =
-      foldl
-        ( \acc expr ->
-            case acc of
-              Left typeError -> Left typeError
-              Right (results, env', context') ->
-                case runExpr language expr env' context' of
-                  Left typeError -> Left typeError
-                  Right (Nothing, env'', context'') ->
-                    Right (results, env'', context'')
-                  Right (Just res, env'', context'') ->
-                    Right (res : results, env'', context'')
-        )
-        (Right ([], env, context))
-        exprs
-
-    runExpr language (Def ident body) env context =
-      let term = evalInEnvWith evaluator env body
-       in case language of
-            Typed ->
-              case infer term of
+ where
+  result =
+    foldl
+      ( \acc expr ->
+          case acc of
+            Left typeError -> Left typeError
+            Right (results, env', context') ->
+              case runExpr expr env' context' of
                 Left typeError -> Left typeError
-                Right typ ->
-                  Right (Nothing, (ident, term) : env, extendContext ident typ context)
-            Untyped ->
-              Right (Nothing, (ident, term) : env, context)
-    runExpr language expr env context =
-      let v = evalInEnvWith evaluator env expr
-       in case language of
-            Typed ->
-              case infer v of
-                Left typeError -> Left typeError
-                Right typ ->
-                  Right (Just (v, typ), env, context)
-            Untyped ->
-              Right (Just (v, TyVar "<?>"), env, context)
+                Right (Nothing, env'', context'') ->
+                  Right (results, env'', context'')
+                Right (Just res, env'', context'') ->
+                  Right (res : results, env'', context'')
+      )
+      (Right ([], env, context))
+      exprs
+
+  runExpr (Def ident body) env' context' =
+    let term = evalInEnvWith evaluator env' body
+     in case language of
+          Typed ->
+            case infer term of
+              Left typeError -> Left typeError
+              Right typ ->
+                Right (Nothing, (ident, term) : env', extendContext ident typ context')
+          Untyped ->
+            Right (Nothing, (ident, term) : env', context')
+  runExpr expr env' context' =
+    let v = evalInEnvWith evaluator env' expr
+     in case language of
+          Typed ->
+            case infer v of
+              Left typeError -> Left typeError
+              Right typ ->
+                Right (Just (v, Just typ), env', context')
+          Untyped ->
+            Right (Just (v, Nothing), env', context')
 
 -- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator.
 -- This is the default evaluator used by the server and REPL.
@@ -74,11 +74,11 @@ evalInEnvWith DeBruijn env expr =
       env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv
    in fromDeBruijn $ eval' env' (toDeBruijn term)
 evalInEnvWith NbE env expr =
-  let term  = desugar expr
+  let term = desugar expr
       -- Build an EnvValue from the user Env by evaluating each binding's
       -- Term in the accumulated value env (builtins always available at the
       -- bottom).  foldl builds left-to-right so earlier bindings are visible
       -- when evaluating later ones.
-      envV  = foldl addBinding builtinEnvValue env
+      envV = foldl addBinding builtinEnvValue env
       addBinding acc (name, t) = (name, Eval.eval acc t) : acc
    in Eval.readBack (Eval.eval envV term)
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
index 96e9990..fa6f1dd 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
@@ -1,11 +1,12 @@
+{-# LANGUAGE DeriveAnyClass #-}
 --  ported from https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE DeriveAnyClass #-}
+
 module Minilang.Lambda.Unify where
 
+import Data.Aeson (FromJSON, ToJSON)
 import Data.Text (Text)
 import GHC.Generics (Generic)
-import Data.Aeson (ToJSON, FromJSON)
 
 type Identifier = Text
 
diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs
index 7da2042..35883b9 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL.hs
@@ -23,34 +23,35 @@ import Minilang.REPL.Pure
 import Minilang.REPL.Purer
 import Minilang.REPL.Run
 import Minilang.REPL.Types
+import System.Console.Haskeline (
+  defaultBehavior,
+  defaultSettings,
+  historyFile,
+  runInputTBehavior,
+  setComplete,
+ )
 import System.Environment (lookupEnv)
-import Text.Read (readMaybe)
-import System.Console.Haskeline
-  ( defaultBehavior,
-    defaultSettings,
-    historyFile,
-    runInputTBehavior,
-    setComplete,
-  )
 import System.IO (Handle, stderr)
+import Text.Read (readMaybe)
 
 -- | Read the evaluator selection from the @MINILANG_EVAL@ environment variable.
 -- Returns 'DeBruijn' when the variable is absent or unrecognised.
 evaluatorFromEnv :: IO Evaluator
 evaluatorFromEnv =
   lookupEnv "MINILANG_EVAL" >>= \case
-    Nothing  -> pure DeBruijn
+    Nothing -> pure DeBruijn
     Just raw -> case readMaybe raw of
       Just ev -> pure ev
       Nothing -> do
         Text.hPutStrLn stderr $
-          "Warning: unknown MINILANG_EVAL value " <> Text.pack (show raw)
-          <> ", falling back to DeBruijn"
+          "Warning: unknown MINILANG_EVAL value "
+            <> Text.pack (show raw)
+            <> ", falling back to DeBruijn"
         pure DeBruijn
 
 -- | Build the initial 'REPLEnv' using the given 'Evaluator'.
 replEnvWith :: Evaluator -> REPLEnv
-replEnvWith ev = initialREPL { evaluator = ev }
+replEnvWith ev = initialREPL{evaluator = ev}
 
 -- * Haskeline REPL
 
@@ -58,8 +59,8 @@ withTerminal :: Evaluator -> IO ()
 withTerminal ev =
   runInputTBehavior defaultBehavior settings $
     evalStateT (runHaskeline runREPL) (replEnvWith ev)
-  where
-    settings = setComplete completion $ defaultSettings {historyFile = Just "~/.minilang.history"}
+ where
+  settings = setComplete completion $ defaultSettings{historyFile = Just "~/.minilang.history"}
 
 -- * Other REPLs
 
@@ -79,9 +80,9 @@ withIO ev hin hout = do
     Right prog -> case loadProgram ev Untyped newEnv newContext prog of
       Right (results, _, _) -> mapM_ (Text.hPutStrLn hout . render) results
       Left err -> Text.hPutStrLn hout (Text.pack $ show err)
-  where
-    render :: (Term, Type) -> Text
-    render (term, _typ) = pretty (resugar term) -- TODO: handle types <> " : " <> Unify.pretty typ
+ where
+  render :: (Term, Maybe Type) -> Text
+  render (term, typ) = pretty (resugar term) <> renderType typ
 
 -- * Pure REPL
 
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
index 8250152..d9dbbbe 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
@@ -13,9 +13,9 @@ import qualified Minilang.Lambda.Unify as Type
 import Minilang.REPL.Types
 
 data PureEnv = PureEnv
-  { inputText :: [Text],
-    outputText :: [Text],
-    pureREPL :: REPLEnv
+  { inputText :: [Text]
+  , outputText :: [Text]
+  , pureREPL :: REPLEnv
   }
 
 newtype PureREPL a = PureREPL {runPure :: CatchT (State PureEnv) a}
@@ -26,25 +26,30 @@ instance MonadREPL PureREPL where
     ins <- gets inputText
     case ins of
       [] -> pure EOF
-      (t : ts) -> modify (\e -> e {inputText = ts}) >> pure (interpret t)
+      (t : ts) -> modify (\e -> e{inputText = ts}) >> pure (interpret t)
 
-  output t = modify $ \e -> e {outputText = render t : outputText e}
+  output t = modify $ \e -> e{outputText = render t : outputText e}
 
   prompt = pure ()
 
   getEnv = gets pureREPL
 
-  setEnv e' = modify $ \e -> e {pureREPL = e'}
+  setEnv e' = modify $ \e -> e{pureREPL = e'}
 
   load f = pure $ Left $ REPLError $ "cannot load file " <> f <> " in Pure interpreter"
 
 render :: Out -> Text
 render = \case
   Msg t -> t
-  Evaluated ast _term typ -> pretty ast <> " : " <> Type.pretty typ
-  Defined ident typ -> ident <> " : " <> Type.pretty typ
+  Evaluated ast _term typ -> pretty ast <> renderType typ
+  Defined ident typ -> ident <> renderType typ
   Bye -> "Bye!"
   other -> pack (show other)
 
+renderType :: Maybe Type.Type -> Text
+renderType typ = case typ of
+  Nothing -> ""
+  Just t -> " : " <> Type.pretty t
+
 instance MonadThrow PureREPL where
   throwM = throw
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index 26f3cad..ba09007 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -8,7 +8,7 @@ module Minilang.REPL.Run where
 
 import Control.Monad.Catch
 import Data.Text hiding (replicate)
-import Minilang.Lambda (loadProgram, evalInEnvWith)
+import Minilang.Lambda (evalInEnvWith, loadProgram)
 import Minilang.Lambda.Eval (newEnv)
 import Minilang.Lambda.Infer (extendContext, infer, newContext)
 import qualified Minilang.Lambda.Infer as Infer
@@ -20,21 +20,21 @@ import Minilang.REPL.Types
 runREPL ::
   (MonadCatch m, MonadREPL m) => m ()
 runREPL = go
-  where
-    go = do
-      prompt
-      raw <- input
-      case raw of
-        EOF -> output Bye
-        In txt -> handleUserInput txt >> go
-        Com cmd -> handleCommand cmd >> go
+ where
+  go = do
+    prompt
+    raw <- input
+    case raw of
+      EOF -> output Bye
+      In txt -> handleUserInput txt >> go
+      Com cmd -> handleCommand cmd >> go
 
 handleUserInput ::
   (MonadCatch m, MonadREPL m) =>
   Text ->
   m ()
 handleUserInput txt = do
-  repl@REPLEnv {language, evaluator, env, context} <- getEnv
+  repl@REPLEnv{language, evaluator, env, context} <- getEnv
   case parse txt of
     Left err -> output (Msg $ pack $ show err)
     Right (Def ident body) -> do
@@ -46,13 +46,13 @@ handleUserInput txt = do
             Right typ -> do
               setEnv $
                 repl
-                  { env = (ident, v) : env,
-                    context = extendContext ident typ context
+                  { env = (ident, v) : env
+                  , context = extendContext ident typ context
                   }
-              output (Defined ident typ)
+              output (Defined ident (Just typ))
         Untyped -> do
-          setEnv $ repl {env = (ident, v) : env}
-          output (Defined ident (TyVar "<?>"))
+          setEnv $ repl{env = (ident, v) : env}
+          output (Defined ident Nothing)
     Right expr -> do
       let v = evalInEnvWith evaluator env expr
           ast = resugar v
@@ -62,17 +62,17 @@ handleUserInput txt = do
             Left typeError -> output (Msg $ Infer.render typeError)
             Right typ -> do
               let
-              output (Evaluated ast v typ)
+              output (Evaluated ast v (Just typ))
         Untyped ->
-          output (Evaluated ast v (TyVar "<?>"))
+          output (Evaluated ast v Nothing)
 
 handleCommand ::
   (MonadCatch m, MonadREPL m) =>
   Command ->
   m ()
-handleCommand ClearEnv = getEnv >>= \e -> setEnv (e {env = newEnv, context = newContext})
+handleCommand ClearEnv = getEnv >>= \e -> setEnv (e{env = newEnv, context = newContext})
 handleCommand DumpEnv =
-  getEnv >>= \REPLEnv {..} ->
+  getEnv >>= \REPLEnv{..} ->
     output (CurrentEnv env context language)
 handleCommand (Load (File file)) = do
   t <- load file
@@ -80,15 +80,15 @@ handleCommand (Load (File file)) = do
     Left err -> output (Msg $ pack $ show err)
     Right prog -> loadProgramInEnv prog
 handleCommand (Load (Data prog)) = loadProgramInEnv prog
-handleCommand (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e {stepTypeCheck = st})
-handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e {debugParser = st})
+handleCommand (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e{stepTypeCheck = st})
+handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e{debugParser = st})
 handleCommand (Set (SelectLanguage lang)) =
   getEnv >>= \e ->
-    setEnv (e {language = lang})
+    setEnv (e{language = lang})
       >> output (Msg $ "Language set to " <> pack (show lang))
 handleCommand (Set (SelectEvaluator ev)) =
   getEnv >>= \e ->
-    setEnv (e {evaluator = ev})
+    setEnv (e{evaluator = ev})
       >> output (Msg $ "Evaluator set to " <> pack (show ev))
 handleCommand Help =
   output (Msg helpText)
@@ -98,12 +98,12 @@ loadProgramInEnv ::
   Text ->
   m ()
 loadProgramInEnv prog = do
-  repl@REPLEnv {env, context, language, evaluator} <- getEnv
+  repl@REPLEnv{env, context, language, evaluator} <- getEnv
   case parseProgram prog of
     Left err -> output (Msg $ pack $ show err)
     Right exprs -> do
       case loadProgram evaluator language env context exprs of
         Left typeError -> output (Msg $ pack $ show typeError)
         Right (results, env', context') -> do
-          setEnv (repl {env = env', context = context'})
+          setEnv (repl{env = env', context = context'})
           mapM_ (\(term, typ) -> output (Evaluated (resugar term) term typ)) results
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index 0b0472e..3bcbbb1 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -7,13 +7,13 @@ import Control.Exception (Exception)
 import Data.Aeson (FromJSON, ToJSON)
 import Data.Text as Text hiding (replicate)
 import GHC.Generics
-import Minilang.Lambda.Eval (Term, Env, newEnv)
+import Minilang.Lambda.Eval (Env, Term, newEnv)
 import Minilang.Lambda.Infer (Context, newContext)
 import Minilang.Lambda.Parser (AST)
 import Minilang.Lambda.Unify (Type)
 import Text.Read (readMaybe)
 
-class (Monad m) => MonadREPL m where
+class Monad m => MonadREPL m where
   -- | Returns the current environment for this session
   -- Environment is made of an `Env`ironment binding names to `Decl`arations
   -- and typing `Context` binding names to `Value`s denoting evaluated types.
@@ -44,13 +44,13 @@ instance Exception REPLError
 
 -- | REPL state
 data REPLEnv = REPLEnv
-  { env :: Env,
-    context :: Context,
-    curIndent :: Int,
-    stepTypeCheck :: Bool,
-    debugParser :: Bool,
-    language :: Language,
-    evaluator :: Evaluator
+  { env :: Env
+  , context :: Context
+  , curIndent :: Int
+  , stepTypeCheck :: Bool
+  , debugParser :: Bool
+  , language :: Language
+  , evaluator :: Evaluator
   }
 
 initialREPL :: REPLEnv
@@ -77,8 +77,8 @@ data Content
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
 data Out
-  = Defined Text Type
-  | Evaluated AST Term Type
+  = Defined Text (Maybe Type)
+  | Evaluated AST Term (Maybe Type)
   | CurrentEnv Env Context Language
   | Msg Text
   | Bye
@@ -128,27 +128,27 @@ interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
 interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) =
   case readMaybe ev of
     Nothing -> Com Help
-    Just e  -> Com $ Set $ SelectEvaluator e
+    Just e -> Com $ Set $ SelectEvaluator e
 interpret t = In t
 
 helpText :: Text
 helpText =
   Text.unlines
-    [ "REPL Commands Help:",
-      "   :h(elp)          : Display this help",
-      "   :q(uit)          : Exit the interpreter",
-      "   :e(nv)           : Displays the current interpreter's environment",
-      "                      This dumps both the Environment, where values are defined,",
-      "                      and the typing Context, where types are defined. ",
-      "   :c(lear)         : Clear the current interpreter's environment",
-      "   :set <option>    : Set an option modifying the interpreter's behaviour",
-      "   :unset <option>  : Remove an option that's been set previously",
-      "   :l(oad) <file>   : load content of <file> into the interpreter, parsing and type-checking it",
-      "   :lang <Language> : Switch type-checking language (Untyped | Typed)",
-      "   :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)",
-      "",
-      "Options: ",
-      "   step             : Run the typechecker step-by-step, pausing at each rule application and",
-      "                      waiting for user to hit <enter> key to continue",
-      "   debug            : Debug parser, displaying the trail of rules tried and triggered"
+    [ "REPL Commands Help:"
+    , "   :h(elp)          : Display this help"
+    , "   :q(uit)          : Exit the interpreter"
+    , "   :e(nv)           : Displays the current interpreter's environment"
+    , "                      This dumps both the Environment, where values are defined,"
+    , "                      and the typing Context, where types are defined. "
+    , "   :c(lear)         : Clear the current interpreter's environment"
+    , "   :set <option>    : Set an option modifying the interpreter's behaviour"
+    , "   :unset <option>  : Remove an option that's been set previously"
+    , "   :l(oad) <file>   : load content of <file> into the interpreter, parsing and type-checking it"
+    , "   :lang <Language> : Switch type-checking language (Untyped | Typed)"
+    , "   :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)"
+    , ""
+    , "Options: "
+    , "   step             : Run the typechecker step-by-step, pausing at each rule application and"
+    , "                      waiting for user to hit <enter> key to continue"
+    , "   debug            : Debug parser, displaying the trail of rules tried and triggered"
     ]