[ highlighting ] case trees in :di (#2440)

2024-12-21 18:51:40 +03:00 · 2022-04-29 12:52:23 +01:00 · 2022-04-29 12:52:23 +01:00 · 4256cd15fd
commit 4256cd15fd
parent 04e65529f6
39 changed files with 604 additions and 239 deletions
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@ -49,6 +49,7 @@ modules =
    Core.Binary.Prims,
    Core.Case.CaseBuilder,
    Core.Case.CaseTree,
+    Core.Case.CaseTree.Pretty,
    Core.Case.Util,
    Core.CompileExpr,
    Core.CompileExpr.Pretty,
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@ -287,12 +287,14 @@ dconFlag n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => throw (InternalError ("Can't find " ++ show n))
-         pure (ciFlags (flags def))
+         pure (ciFlags (definition def) (flags def))
  where
-    ciFlags : List DefFlag -> ConInfo
-    ciFlags [] = DATACON
-    ciFlags (ConType ci :: xs) = ci
-    ciFlags (x :: xs) = ciFlags xs
+    ciFlags : Def -> List DefFlag -> ConInfo
+    ciFlags def [] = case def of
+      TCon{} => TYCON
+      _ => DATACON
+    ciFlags def (ConType ci :: xs) = ci
+    ciFlags def (x :: xs) = ciFlags def xs

 mutual
  toCExpTm : {vars : _} ->
--- a/src/Core/Case/CaseTree.idr
+++ b/src/Core/Case/CaseTree.idr
@ -143,32 +143,6 @@ covering
 {vars : _} -> Show (CaseAlt vars) where
  show = showCA ""

-mutual
-  export
-  {vars : _} -> Pretty IdrisSyntax (CaseTree vars) where
-    pretty (Case {name} idx prf ty alts)
-      = case_ <++> pretty0 name <++> keyword ":" <++> byShow ty <++> of_
-         <+> nest 2 (hardline
-         <+> vsep (assert_total (map pretty alts)))
-    pretty (STerm i tm) = byShow tm
-    pretty (Unmatched msg) = "Error:" <++> pretty0 msg
-    pretty Impossible = "Impossible"
-
-  export
-  {vars : _} -> Pretty IdrisSyntax (CaseAlt vars) where
-    pretty (ConCase n tag args sc)
-      = hsep (map pretty0 (n :: args)) <++> fatArrow
-        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
-    pretty (DelayCase _ arg sc) =
-        keyword "Delay" <++> pretty0 arg <++> fatArrow
-        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
-    pretty (ConstCase c sc) =
-        pretty c <++> fatArrow
-        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
-    pretty (DefaultCase sc) =
-        keyword "_" <++> fatArrow
-        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
-
 mutual
  export
  eqTree : CaseTree vs -> CaseTree vs' -> Bool
--- a/src/Core/Case/CaseTree/Pretty.idr
+++ b/src/Core/Case/CaseTree/Pretty.idr
@ -0,0 +1,104 @@
+module Core.Case.CaseTree.Pretty
+
+import Core.Context
+import Core.Env
+import Core.TT
+import Core.Case.CaseTree
+import Idris.Syntax
+import Idris.Pretty
+import Idris.Resugar
+
+import Data.String
+import Libraries.Data.String.Extra
+import Libraries.Text.PrettyPrint.Prettyprinter
+
+namespace Raw
+
+  export
+  prettyTree : {vars : _} -> CaseTree vars -> Doc IdrisSyntax
+  prettyAlt : {vars : _} -> CaseAlt vars -> Doc IdrisSyntax
+
+  prettyTree (Case {name} idx prf ty alts)
+      = let ann = case ty of
+                    Erased _ _ => ""
+                    _ => space <+> keyword ":" <++> byShow ty
+        in case_ <++> annotate Bound (pretty0 name) <+> ann <++> of_
+         <+> nest 2 (hardline
+         <+> vsep (assert_total (map prettyAlt alts)))
+  prettyTree (STerm i tm) = byShow tm
+  prettyTree (Unmatched msg) = "Error:" <++> pretty0 msg
+  prettyTree Impossible = "Impossible"
+
+  prettyAlt (ConCase n tag args sc)
+      = hsep (annotate (DCon (Just n)) (pretty0 n) ::  map pretty0 args)
+        <++> fatArrow
+        <+> let sc = prettyTree sc in
+            Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt (DelayCase _ arg sc) =
+        keyword "Delay" <++> pretty0 arg
+        <++> fatArrow
+        <+> let sc = prettyTree sc in
+            Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt (ConstCase c sc) =
+        pretty c
+        <++> fatArrow
+        <+> let sc = prettyTree sc in
+            Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt (DefaultCase sc) =
+        keyword "_"
+        <++> fatArrow
+        <+> let sc = prettyTree sc in
+            Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+
+namespace Resugared
+
+  prettyName : {auto c : Ref Ctxt Defs} ->
+               Name -> Core (Doc IdrisSyntax)
+  prettyName nm
+    = pure $ ifThenElse (fullNamespace !(getPPrint))
+               (pretty0 nm)
+               (cast $ prettyOp True $ dropNS nm)
+
+  export
+  prettyTree : {vars : _} ->
+    {auto c : Ref Ctxt Defs} ->
+    {auto s : Ref Syn SyntaxInfo} ->
+    Env Term vars -> CaseTree vars -> Core (Doc IdrisSyntax)
+  prettyAlt : {vars : _} ->
+    {auto c : Ref Ctxt Defs} ->
+    {auto s : Ref Syn SyntaxInfo} ->
+    Env Term vars -> CaseAlt vars -> Core (Doc IdrisSyntax)
+
+  prettyTree env (Case {name} idx prf ty alts) = do
+    ann <- case ty of
+             Erased _ _ => pure ""
+             _ => do ty <- resugar env ty
+                     pure (space <+> keyword ":" <++> pretty ty)
+    alts <- assert_total (traverse (prettyAlt env) alts)
+    pure $ case_ <++> pretty0 name <+> ann <++> of_
+       <+> nest 2 (hardline <+> vsep alts)
+  prettyTree env (STerm i tm) = pretty <$> resugar env tm
+  prettyTree env (Unmatched msg) = pure ("Error:" <++> pretty0 msg)
+  prettyTree env Impossible = pure "Impossible"
+
+  prettyAlt env (ConCase n tag args sc) = do
+    con <- prettyName n
+    sc <- prettyTree (mkEnvOnto emptyFC args env) sc
+    pure $ hsep (annotate (DCon (Just n)) con ::  map pretty0 args)
+     <++> fatArrow
+      <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt env (DelayCase _ arg sc) = do
+    sc <- prettyTree (mkEnvOnto emptyFC [_,_] env) sc
+    pure $ keyword "Delay" <++> pretty0 arg
+        <++> fatArrow
+        <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt env (ConstCase c sc) = do
+    sc <- prettyTree env sc
+    pure $ pretty c
+        <++> fatArrow
+        <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
+  prettyAlt env (DefaultCase sc) = do
+    sc <- prettyTree env sc
+    pure $ keyword "_"
+        <++> fatArrow
+        <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
--- a/src/Core/CompileExpr/Pretty.idr
+++ b/src/Core/CompileExpr/Pretty.idr
@ -37,21 +37,22 @@ import Libraries.Data.String.Extra
 %hide Pretty.Syntax
 %hide List1.forget

-prettyFlag : ConInfo -> Doc ann
-prettyFlag DATACON = ""
-prettyFlag f = pretty0 (show f)
+prettyFlag : ConInfo -> Maybe (Doc ann)
+prettyFlag DATACON = Nothing
+prettyFlag f = Just (byShow f)

 prettyCon : Name -> ConInfo -> Maybe Int -> Doc IdrisSyntax
-prettyCon x ci tag
-  = hsep [ annotate (DCon (Just x)) (pretty0 x)
-         , braces ("tag =" <++> byShow tag)
-         , prettyFlag ci
-         ]
+prettyCon x ci mtag
+  = hsep $ catMaybes
+      [ Just (annotate ((if ci == TYCON then TCon else DCon) (Just x)) (pretty0 x))
+      , (braces . ("tag =" <++>) . byShow) <$> mtag
+      , prettyFlag ci
+      ]

 mutual
  Pretty IdrisSyntax NamedCExp where
-    prettyPrec d (NmLocal _ x) = "!" <+> pretty0 x
-    prettyPrec d (NmRef _ x) = pretty0 x
+    prettyPrec d (NmLocal _ x) = annotate Bound $ pretty0 x
+    prettyPrec d (NmRef _ x) = annotate (Fun x) $ pretty0 x
    prettyPrec d (NmLam _ x y)
      = parenthesise (d > Open) $ keyword "\\" <+> pretty0 x <+> fatArrow <++> pretty y
    prettyPrec d (NmLet _ x y z)
@ -82,7 +83,8 @@ mutual
    prettyPrec d (NmErased _) = "___"
    prettyPrec d (NmCrash _ x)
        = parenthesise (d > Open) $
-            sep ["crash", pretty0 x]
+            sep [annotate Keyword "crash", byShow x]
+
  Pretty IdrisSyntax NamedConAlt where
    pretty (MkNConAlt x ci tag args exp)
        = sep (prettyCon x ci tag :: map pretty0 args ++ [fatArrow <+> softline <+> align (pretty exp) ])
--- a/src/Core/Context/Pretty.idr
+++ b/src/Core/Context/Pretty.idr
@ -1,15 +1,22 @@
 module Core.Context.Pretty

+import Core.Context
+import Core.Env
+
 import Data.String
 import Idris.Doc.Annotations

+import Idris.Syntax
 import Idris.Pretty

 import Core.Case.CaseTree
+import Core.Case.CaseTree.Pretty
 import Core.Context.Context

 import Libraries.Data.String.Extra

+%hide Env.(::)
+%hide Env.Nil
 %hide String.(::)
 %hide String.Nil
 %hide Doc.Nil
@ -29,49 +36,103 @@ import Libraries.Data.String.Extra

 %default covering

-export
-Pretty IdrisDocAnn Def where
-  pretty None = "undefined"
-  pretty (PMDef _ args ct _ pats)
-    = vcat [ "Arguments" <++> cast (prettyList args)
-           , header "Compile time tree" <++> prettyBy Syntax ct
-           ]
-  pretty (DCon tag arity nt)
-    = vcat $ header "Data constructor" :: map (indent 2)
-        ([ "tag:" <++> byShow tag
-         , "arity:" <++> byShow arity
-         ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
-  pretty (TCon tag arity ps ds u ms cons det)
-    = let enum = hsep . punctuate "," in
-      vcat $ header "Type constructor" :: map (indent 2)
-        ([ "tag:" <++> byShow tag
-         , "arity:" <++> byShow arity
-         , "parameter positions:" <++> byShow ps
-         , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
-         ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
-           ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
-  pretty (ExternDef arity)
-    = vcat $ header "External definition" :: map (indent 2)
-         [ "arity:" <++> byShow arity ]
-  pretty (ForeignDef arity calls)
-    = vcat $ header "Foreign definition" :: map (indent 2)
-        [ "arity:" <++> byShow arity
-        , "bindings:" <++> byShow calls ]
-  pretty (Builtin {arity} _)
-    = vcat $ header "Builtin" :: map (indent 2)
-        [ "arity:" <++> byShow arity ]
-  pretty (Hole numlocs hf)
-    = vcat $ header "Hole" :: map (indent 2)
-        ("Implicitly bound name" <$ guard (implbind hf))
-  pretty (BySearch rig depth def)
-    = vcat $ header "Search" :: map (indent 2)
-        [ "depth:" <++> byShow depth
-        , "in:" <++> pretty0 def ]
-  pretty (Guess tm _ cs)
-    = vcat $ header "Guess" :: map (indent 2)
-        [ "solution:" <++> byShow tm
-        , "when:" <++> byShow cs ]
-  pretty (UniverseLevel i)
-    = "Universe level #" <+> byShow i
-  pretty ImpBind = "Bound name"
-  pretty Delayed = "Delayed"
+namespace Raw
+  export
+  prettyDef : Def -> Doc IdrisDocAnn
+  prettyDef None = "undefined"
+  prettyDef (PMDef _ args ct _ pats) =
+       let ct = prettyTree ct in
+       vcat
+        [ "Arguments" <++> cast (prettyList args)
+        , header "Compile time tree" <++> reAnnotate Syntax ct
+        ]
+  prettyDef (DCon tag arity nt) =
+      vcat $ header "Data constructor" :: map (indent 2)
+          ([ "tag:" <++> byShow tag
+           , "arity:" <++> byShow arity
+           ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
+  prettyDef (TCon tag arity ps ds u ms cons det) =
+        let enum = hsep . punctuate "," in
+        vcat $ header "Type constructor" :: map (indent 2)
+          ([ "tag:" <++> byShow tag
+           , "arity:" <++> byShow arity
+           , "parameter positions:" <++> byShow ps
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
+             ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
+  prettyDef (ExternDef arity) =
+      vcat $ header "External definition" :: map (indent 2)
+           [ "arity:" <++> byShow arity ]
+  prettyDef (ForeignDef arity calls) =
+     vcat $ header "Foreign definition" :: map (indent 2)
+          [ "arity:" <++> byShow arity
+          , "bindings:" <++> byShow calls ]
+  prettyDef (Builtin {arity} _) =
+        vcat $ header "Builtin" :: map (indent 2)
+          [ "arity:" <++> byShow arity ]
+  prettyDef (Hole numlocs hf) =
+        vcat $ header "Hole" :: map (indent 2)
+          ("Implicitly bound name" <$ guard (implbind hf))
+  prettyDef (BySearch rig depth def) =
+        vcat $ header "Search" :: map (indent 2)
+          [ "depth:" <++> byShow depth
+          , "in:" <++> pretty0 def ]
+  prettyDef (Guess tm _ cs) =
+        vcat $ header "Guess" :: map (indent 2)
+          [ "solution:" <++> byShow tm
+          , "when:" <++> byShow cs ]
+  prettyDef (UniverseLevel i) = "Universe level #" <+> byShow i
+  prettyDef ImpBind = "Bound name"
+  prettyDef Delayed = "Delayed"
+
+namespace Resugared
+
+  export
+  prettyDef : {auto c : Ref Ctxt Defs} ->
+              {auto s : Ref Syn SyntaxInfo} ->
+              Def -> Core (Doc IdrisDocAnn)
+  prettyDef None = pure "undefined"
+  prettyDef (PMDef _ args ct _ pats) = do
+      ct <- prettyTree (mkEnv emptyFC _) ct
+      pure $ vcat
+        [ "Arguments" <++> cast (prettyList args)
+        , header "Compile time tree" <++> reAnnotate Syntax ct
+        ]
+  prettyDef (DCon tag arity nt) = pure $
+      vcat $ header "Data constructor" :: map (indent 2)
+          ([ "tag:" <++> byShow tag
+           , "arity:" <++> byShow arity
+           ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
+  prettyDef (TCon tag arity ps ds u ms cons det) = pure $
+        let enum = hsep . punctuate "," in
+        vcat $ header "Type constructor" :: map (indent 2)
+          ([ "tag:" <++> byShow tag
+           , "arity:" <++> byShow arity
+           , "parameter positions:" <++> byShow ps
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
+             ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
+  prettyDef (ExternDef arity) = pure $
+      vcat $ header "External definition" :: map (indent 2)
+           [ "arity:" <++> byShow arity ]
+  prettyDef (ForeignDef arity calls) = pure $
+     vcat $ header "Foreign definition" :: map (indent 2)
+          [ "arity:" <++> byShow arity
+          , "bindings:" <++> byShow calls ]
+  prettyDef (Builtin {arity} _) = pure $
+        vcat $ header "Builtin" :: map (indent 2)
+          [ "arity:" <++> byShow arity ]
+  prettyDef (Hole numlocs hf) = pure $
+        vcat $ header "Hole" :: map (indent 2)
+          ("Implicitly bound name" <$ guard (implbind hf))
+  prettyDef (BySearch rig depth def) = pure $
+        vcat $ header "Search" :: map (indent 2)
+          [ "depth:" <++> byShow depth
+          , "in:" <++> pretty0 def ]
+  prettyDef (Guess tm _ cs) = pure $
+        vcat $ header "Guess" :: map (indent 2)
+          [ "solution:" <++> byShow tm
+          , "when:" <++> byShow cs ]
+  prettyDef (UniverseLevel i) = pure $ "Universe level #" <+> byShow i
+  prettyDef ImpBind = pure "Bound name"
+  prettyDef Delayed = pure "Delayed"
--- a/src/Core/Env.idr
+++ b/src/Core/Env.idr
@ -17,6 +17,7 @@ export
 extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 extend x = (::) {x}

+
 export
 length : Env tm xs -> Nat
 length [] = 0
@ -250,6 +251,13 @@ shrinkEnv (b :: env) (KeepCons p)
         b' <- assert_total (shrinkBinder b p)
         pure (b' :: env')

+export
+mkEnvOnto : FC -> (xs : List Name) -> Env Term ys -> Env Term (xs ++ ys)
+mkEnvOnto fc [] vs = vs
+mkEnvOnto fc (n :: ns) vs
+   = PVar fc top Explicit (Erased fc False)
+   :: mkEnvOnto fc ns vs
+
 -- Make a dummy environment, if we genuinely don't care about the values
 -- and types of the contents.
 -- We use this when building and comparing case trees.
--- a/src/Core/Name.idr
+++ b/src/Core/Name.idr
@ -287,11 +287,11 @@ mutual
  Pretty Void Name where
    pretty (NS ns n) = pretty ns <+> dot <+> prettyOp True n
    pretty (UN x) = pretty x
-    pretty (MN x y) = braces (pretty x <+> colon <+> pretty (show y))
-    pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty (show d))
+    pretty (MN x y) = braces (pretty x <+> colon <+> byShow y)
+    pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> byShow d)
    pretty (DN str _) = pretty str
    pretty (Nested (outer, idx) inner)
-      = pretty (show outer) <+> colon <+> pretty (show idx) <+> colon <+> pretty inner
+      = byShow outer <+> colon <+> byShow idx <+> colon <+> pretty inner
    pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
    pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
    pretty (Resolved x) = pretty "$resolved" <+> pretty (show x)
--- a/src/Core/Options.idr
+++ b/src/Core/Options.idr
@ -184,6 +184,7 @@ public export
 record PPrinter where
  constructor MkPPOpts
  showImplicits : Bool
+  showMachineNames : Bool
  showFullEnv : Bool
  fullNamespace : Bool

@ -222,7 +223,7 @@ defaultDirs = MkDirs "." Nothing "build" "depends" Nothing
                     "/usr/local" ["."] [] [] []

 defaultPPrint : PPrinter
-defaultPPrint = MkPPOpts False True False
+defaultPPrint = MkPPOpts False False True False

 export
 defaultSession : Session
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@ -429,45 +429,45 @@ Show (PrimFn arity) where

 export
 prettyOp : PrimFn arity -> Vect arity (Doc IdrisSyntax) -> Doc IdrisSyntax
-prettyOp (Add ty) [v1,v2] = v1 <++> "+" <++> v2
-prettyOp (Sub ty) [v1,v2] = v1 <++> "-" <++> v2
-prettyOp (Mul ty) [v1,v2] = v1 <++> "*" <++> v2
-prettyOp (Div ty) [v1,v2] = v1 <++> "`div`" <++> v2
-prettyOp (Mod ty) [v1,v2] = v1 <++> "`mod`" <++> v2
-prettyOp (Neg ty) [v] = "-" <++> v
-prettyOp (ShiftL ty) [v1,v2] = "shiftl" <++> v1 <++> v2
-prettyOp (ShiftR ty) [v1,v2] = "shiftr" <++> v1 <++> v2
-prettyOp (BAnd ty) [v1,v2] = v1 <++> "&&" <++> v2
-prettyOp (BOr ty) [v1,v2] = v1 <++> "||" <++> v2
-prettyOp (BXOr ty) [v1,v2] = v1 <++> "`xor`" <++> v2
-prettyOp (LT ty) [v1,v2] = v1 <++> "<" <++> v2
-prettyOp (LTE ty) [v1,v2] = v1 <++> "<=" <++> v2
-prettyOp (EQ ty) [v1,v2] = v1 <++> "==" <++> v2
-prettyOp (GTE ty) [v1,v2] = v1 <++> ">=" <++> v2
-prettyOp (GT ty) [v1,v2] = v1 <++> ">" <++> v2
-prettyOp StrLength [v] = "length" <++> v
-prettyOp StrHead [v] = "head" <++> v
-prettyOp StrTail [v] = "tail" <++> v
-prettyOp StrIndex [v1,v2] = v1 <++> "[" <+> v2 <+> "]"
-prettyOp StrCons [v1,v2] = v1 <++> "::" <++> v2
-prettyOp StrAppend [v1,v2] = v1 <++> "++" <++> v2
-prettyOp StrReverse [v] = "reverse" <++> v
-prettyOp StrSubstr [v1,v2,v3] = v1 <++> "[" <+> v2 <+> "," <++> v3 <+> "]"
-prettyOp DoubleExp [v] = "exp" <++> v
-prettyOp DoubleLog [v] = "log" <++> v
-prettyOp DoublePow [v1,v2] = v1 <++> "`pow`" <++> v2
-prettyOp DoubleSin [v] = "sin" <++> v
-prettyOp DoubleCos [v] = "cos" <++> v
-prettyOp DoubleTan [v] = "tan" <++> v
-prettyOp DoubleASin [v] = "asin" <++> v
-prettyOp DoubleACos [v] = "acos" <++> v
-prettyOp DoubleATan [v] = "atan" <++> v
-prettyOp DoubleSqrt [v] = "sqrt" <++> v
-prettyOp DoubleFloor [v] = "floor" <++> v
-prettyOp DoubleCeiling [v] = "ceiling" <++> v
-prettyOp (Cast x y) [v] = "[" <+> pretty x <++> "->" <++> pretty y <+> "]" <++> v
-prettyOp BelieveMe [v1,v2,v3] = "believe_me" <++> v1 <++> v2 <++> v3
-prettyOp Crash [v1,v2] = "crash" <++> v1 <++> v2
+prettyOp op@(Add ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "+" <++> v2
+prettyOp op@(Sub ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "-" <++> v2
+prettyOp op@(Mul ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "*" <++> v2
+prettyOp op@(Div ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`div`" <++> v2
+prettyOp op@(Mod ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`mod`" <++> v2
+prettyOp op@(Neg ty) [v] = annotate (Fun $ UN $ Basic $ show op) "-" <++> v
+prettyOp op@(ShiftL ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftl" <++> v1 <++> v2
+prettyOp op@(ShiftR ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftr" <++> v1 <++> v2
+prettyOp op@(BAnd ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "&&" <++> v2
+prettyOp op@(BOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "||" <++> v2
+prettyOp op@(BXOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`xor`" <++> v2
+prettyOp op@(LT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<" <++> v2
+prettyOp op@(LTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<=" <++> v2
+prettyOp op@(EQ ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "==" <++> v2
+prettyOp op@(GTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">=" <++> v2
+prettyOp op@(GT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">" <++> v2
+prettyOp op@StrLength [v] = annotate (Fun $ UN $ Basic $ show op) "length" <++> v
+prettyOp op@StrHead [v] = annotate (Fun $ UN $ Basic $ show op) "head" <++> v
+prettyOp op@StrTail [v] = annotate (Fun $ UN $ Basic $ show op) "tail" <++> v
+prettyOp op@StrIndex [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "]"
+prettyOp op@StrCons [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "::" <++> v2
+prettyOp op@StrAppend [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "++" <++> v2
+prettyOp op@StrReverse [v] = annotate (Fun $ UN $ Basic $ show op) "reverse" <++> v
+prettyOp op@StrSubstr [v1,v2,v3] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "," <++> v3 <+> annotate (Fun $ UN $ Basic $ show op) "]"
+prettyOp op@DoubleExp [v] = annotate (Fun $ UN $ Basic $ show op) "exp" <++> v
+prettyOp op@DoubleLog [v] = annotate (Fun $ UN $ Basic $ show op) "log" <++> v
+prettyOp op@DoublePow [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`pow`" <++> v2
+prettyOp op@DoubleSin [v] = annotate (Fun $ UN $ Basic $ show op) "sin" <++> v
+prettyOp op@DoubleCos [v] = annotate (Fun $ UN $ Basic $ show op) "cos" <++> v
+prettyOp op@DoubleTan [v] = annotate (Fun $ UN $ Basic $ show op) "tan" <++> v
+prettyOp op@DoubleASin [v] = annotate (Fun $ UN $ Basic $ show op) "asin" <++> v
+prettyOp op@DoubleACos [v] = annotate (Fun $ UN $ Basic $ show op) "acos" <++> v
+prettyOp op@DoubleATan [v] = annotate (Fun $ UN $ Basic $ show op) "atan" <++> v
+prettyOp op@DoubleSqrt [v] = annotate (Fun $ UN $ Basic $ show op) "sqrt" <++> v
+prettyOp op@DoubleFloor [v] = annotate (Fun $ UN $ Basic $ show op) "floor" <++> v
+prettyOp op@DoubleCeiling [v] = annotate (Fun $ UN $ Basic $ show op) "ceiling" <++> v
+prettyOp op@(Cast x y) [v] = annotate (Fun $ UN $ Basic $ show op) "[" <+> pretty x <++> annotate (Fun $ UN $ Basic $ show op) "->" <++> pretty y <+> annotate (Fun $ UN $ Basic $ show op) "]" <++> v
+prettyOp op@BelieveMe [v1,v2,v3] = annotate (Fun $ UN $ Basic $ show op) "believe_me" <++> v1 <++> v2 <++> v3
+prettyOp op@Crash [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "crash" <++> v1 <++> v2


 public export
--- a/src/Idris/CommandLine.idr
+++ b/src/Idris/CommandLine.idr
@ -94,6 +94,10 @@ data CLOpt
  NoBanner |
   ||| Run Idris 2 in quiet mode
  Quiet |
+   ||| Show machine names when pretty printing
+  ShowMachineNames |
+   ||| Show namespaces when pretty printing
+  ShowNamespaces |
   ||| Run Idris 2 in verbose mode (cancels quiet if it's the default)
  Verbose |
   ||| Set the console width for REPL output
@ -267,7 +271,6 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
           MkOpt ["--init"] [Optional "package file"]
              (\ f => [Package Init f])
              (Just "Interactively initialise a new project"),
-
           MkOpt ["--build"] [Optional "package file"]
               (\f => [Package Build f])
              (Just "Build modules/executable for the given package"),
@ -313,6 +316,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
              (Just "Quiet mode; display fewer messages"),
           MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l])
              (Just "Width for console output (0 for unbounded) (auto by default)"),
+           MkOpt ["--show-machine-names"] [] [ShowMachineNames]
+              (Just "Show machine names when pretty printing"),
+           MkOpt ["--show-namespaces"] [] [ShowNamespaces]
+              (Just "Show namespaces when pretty printing"),
           MkOpt ["--color", "--colour"] [] ([Color True])
              (Just "Forces colored console output (enabled by default)"),
           MkOpt ["--no-color", "--no-colour"] [] ([Color False])
--- a/src/Idris/Doc/Display.idr
+++ b/src/Idris/Doc/Display.idr
@ -1,6 +1,7 @@
 module Idris.Doc.Display

 import Core.Case.CaseTree
+import Core.Case.CaseTree.Pretty
 import Core.Context
 import Core.Env

--- a/src/Idris/IDEMode/Holes.idr
+++ b/src/Idris/IDEMode/Holes.idr
@ -27,24 +27,16 @@ impBracket : Bool -> String -> String
 impBracket False str = str
 impBracket True str = "{" ++ str ++ "}"

-tidy : Name -> String
-tidy (MN n _) = n
-tidy n = show n
-
 export covering
 Show Holes.Premise where
  show premise =
    " " ++ showCount premise.multiplicity ++ " "
-    ++ impBracket premise.isImplicit (tidy premise.name ++ " : " ++ show premise.type)
+    ++ impBracket premise.isImplicit (show premise.name ++ " : " ++ show premise.type)

 prettyImpBracket : Bool -> Doc ann -> Doc ann
 prettyImpBracket False = id
 prettyImpBracket True = braces

-prettyName : Name -> Doc IdrisSyntax
-prettyName (MN n _) = pretty0 n
-prettyName n = pretty0 n
-
 export
 prettyRigHole : RigCount -> Doc IdrisSyntax
 prettyRigHole = elimSemi (keyword (pretty0 '0') <+> space)
@ -55,7 +47,7 @@ export
 Pretty IdrisSyntax Holes.Premise where
  pretty premise =
     prettyRigHole premise.multiplicity
-     <+> prettyImpBracket premise.isImplicit (prettyName premise.name <++> colon <++> pretty premise.type)
+     <+> prettyImpBracket premise.isImplicit (pretty0 premise.name <++> colon <++> pretty premise.type)

 public export
 record Data where
@ -201,7 +193,7 @@ premiseIDE : Holes.Premise -> HolePremise
 premiseIDE premise = IDE.MkHolePremise
  { name = " " ++ showCount premise.multiplicity ++ " "
               ++ (impBracket premise.isImplicit $
-                  tidy premise.name)
+                  show premise.name)
  , type = show premise.type
  }

--- a/src/Idris/IDEMode/REPL.idr
+++ b/src/Idris/IDEMode/REPL.idr
@ -290,14 +290,15 @@ Cast REPLEval String where
  cast Scheme = "scheme"

 Cast REPLOpt REPLOption where
-  cast (ShowImplicits impl) = MkOption "show-implicits" BOOL impl
-  cast (ShowNamespace ns)   = MkOption "show-namespace" BOOL ns
-  cast (ShowTypes typs)     = MkOption "show-types"     BOOL typs
-  cast (EvalMode mod)       = MkOption "eval"           ATOM $ cast mod
-  cast (Editor editor)      = MkOption "editor"         STRING editor
-  cast (CG str)             = MkOption "cg"             STRING str
-  cast (Profile p)          = MkOption "profile"        BOOL p
-  cast (EvalTiming p)       = MkOption "evaltiming"     BOOL p
+  cast (ShowImplicits impl)  = MkOption "show-implicits" BOOL impl
+  cast (ShowNamespace ns)    = MkOption "show-namespace" BOOL ns
+  cast (ShowMachineNames ns) = MkOption "show-machinenames" BOOL ns
+  cast (ShowTypes typs)      = MkOption "show-types"     BOOL typs
+  cast (EvalMode mod)        = MkOption "eval"           ATOM $ cast mod
+  cast (Editor editor)       = MkOption "editor"         STRING editor
+  cast (CG str)              = MkOption "cg"             STRING str
+  cast (Profile p)           = MkOption "profile"        BOOL p
+  cast (EvalTiming p)        = MkOption "evaltiming"     BOOL p


 displayIDEResult : {auto c : Ref Ctxt Defs} ->
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@ -494,7 +494,7 @@ makeDoc pkg opts =
       Right () <- coreLift $ mkdirAll docDir
         | Left err => fileError docDir err
       u <- newRef UST initUState
-       setPPrint (MkPPOpts False False False)
+       setPPrint (MkPPOpts False True False False)

       [] <- concat <$> for (modules pkg) (\(mod, filename) => do
           -- load dependencies
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@ -1905,6 +1905,8 @@ setOption set
         pure (ShowImplicits set)
  <|> do exactIdent "shownamespace"
         pure (ShowNamespace set)
+  <|> do exactIdent "showmachinenames"
+         pure (ShowMachineNames set)
  <|> do exactIdent "showtypes"
         pure (ShowTypes set)
  <|> do exactIdent "profile"
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@ -101,16 +101,21 @@ showInfo (n, idx, d)
                        "Size change: " ++ showSep ", " scinfo

 prettyInfo : {auto c : Ref Ctxt Defs} ->
-           (Name, Int, GlobalDef) -> Core (Doc IdrisDocAnn)
+             {auto s : Ref Syn SyntaxInfo} ->
+             (Name, Int, GlobalDef) -> Core (Doc IdrisDocAnn)
 prettyInfo (n, idx, d)
    = do let nm = fullname d
         def <- toFullNames (definition d)
         referCT <- traverse getFullName (keys (refersTo d))
         referRT <- traverse getFullName (keys (refersToRuntime d))
         schanges <- traverse toFullNames $ sizeChange d
+         pp <- getPPrint
+         setPPrint ({ showMachineNames := True } pp)
+         def <- Resugared.prettyDef def
+         setPPrint ({ showMachineNames := showMachineNames pp } pp)
         pure $ vcat $
           [ reAnnotate Syntax (prettyRig $ multiplicity d) <+> showCategory Syntax d (pretty0 nm)
-           , pretty def
+           , def
           ] ++
           catMaybes
           [ (\ args => header "Erasable args" <++> byShow args) <$> ifNotNull (eraseArgs d)
@ -162,6 +167,9 @@ setOpt (ShowImplicits t)
 setOpt (ShowNamespace t)
    = do pp <- getPPrint
         setPPrint ({ fullNamespace := t } pp)
+setOpt (ShowMachineNames t)
+    = do pp <- getPPrint
+         setPPrint ({ showMachineNames := t } pp)
 setOpt (ShowTypes t)
    = update ROpts { showTypes := t }
 setOpt (EvalMode m)
--- a/src/Idris/Resugar.idr
+++ b/src/Idris/Resugar.idr
@ -98,12 +98,6 @@ showFullEnv
    = do pp <- getPPrint
         pure (showFullEnv pp)

-fullNamespace : {auto c : Ref Ctxt Defs} ->
-                Core Bool
-fullNamespace
-    = do pp <- getPPrint
-         pure (fullNamespace pp)
-
 unbracket : PTerm' nm -> PTerm' nm
 unbracket (PBracketed _ tm) = tm
 unbracket tm = tm
@ -111,11 +105,11 @@ unbracket tm = tm
 ||| Attempt to extract a constant natural number
 extractNat : Nat -> IPTerm -> Maybe Nat
 extractNat acc tm = case tm of
-  PRef _ (MkKindedName _ _ (NS ns (UN (Basic n)))) =>
+  PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn) =>
    do guard (n == "Z")
       guard (ns == typesNS || ns == preludeNS)
       pure acc
-  PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of
+  PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of
    "S" => do guard (ns == typesNS || ns == preludeNS)
              extractNat (1 + acc) k
    "fromInteger" => extractNat acc k
@ -128,7 +122,7 @@ extractNat acc tm = case tm of
 ||| Attempt to extract a constant integer
 extractInteger : IPTerm -> Maybe Integer
 extractInteger tm = case tm of
-  PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of
+  PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of
    "fromInteger" => extractInteger k
    "negate"      => negate <$> extractInteger k
    _ => Nothing
@ -139,7 +133,7 @@ extractInteger tm = case tm of
 ||| Attempt to extract a constant double
 extractDouble : IPTerm -> Maybe Double
 extractDouble tm = case tm of
-  PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of
+  PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of
    "fromDouble" => extractDouble k
    "negate"     => negate <$> extractDouble k
    _ => Nothing
@ -152,11 +146,11 @@ mutual
  ||| Put the special names (Nil, ::, Pair, Z, S, etc) back as syntax
  ||| Returns `Nothing` in case there was nothing to resugar.
  sugarAppM : IPTerm -> Maybe IPTerm
-  sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) m) r) =
+  sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) m) r) =
    case nameRoot nm of
      "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r)
      _ => Nothing
-  sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) r) =
+  sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) r) =
    if builtinNS == ns
       then case nameRoot nm of
         "Pair"   => pure $ PPair fc (unbracket l) (unbracket r)
@ -189,7 +183,7 @@ mutual
        Nothing = extractDouble tm
          | Just d => pure $ PPrimVal (getPTermLoc tm) (Db d)
    in case tm of
-        PRef fc (MkKindedName nt _ (NS ns nm)) =>
+        PRef fc (MkKindedName nt (NS ns nm) rn) =>
          if builtinNS == ns
             then case nameRoot nm of
               "Unit"   => pure $ PUnit fc
@ -199,7 +193,7 @@ mutual
               "Nil" => pure $ PList fc fc []
               "Lin" => pure $ PSnocList fc fc [<]
               _     => Nothing
-        PApp fc (PRef _ (MkKindedName nt _ (NS ns nm))) arg =>
+        PApp fc (PRef _ (MkKindedName nt (NS ns nm) rn)) arg =>
          case nameRoot nm of
            "rangeFrom" => pure $ PRangeStream fc (unbracket arg) Nothing
            _           => Nothing
@ -218,12 +212,12 @@ sugarName (DN n _) = n
 sugarName x = show x

 toPRef : FC -> KindedName -> Core IPTerm
-toPRef fc kn@(MkKindedName nt fn nm) = case nm of
-  MN n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n)))
+toPRef fc (MkKindedName nt fn nm) = case dropNS nm of
+  MN n i     => pure (sugarApp (PRef fc (MkKindedName nt fn $ MN n i)))
  PV n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ n)))
  DN n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n)))
  Nested _ n => toPRef fc (MkKindedName nt fn n)
-  _          => pure (sugarApp (PRef fc kn))
+  n          => pure (sugarApp (PRef fc (MkKindedName nt fn n)))

 mutual
  toPTerm : {auto c : Ref Ctxt Defs} ->
@ -524,17 +518,19 @@ export
 cleanPTerm : {auto c : Ref Ctxt Defs} ->
             IPTerm -> Core IPTerm
 cleanPTerm ptm
-   = do ns <- fullNamespace
-        if ns then pure ptm else mapPTermM cleanNode ptm
+   = do pp <- getPPrint
+        if showMachineNames pp then pure ptm else mapPTermM cleanNode ptm

  where

    cleanName : Name -> Core Name
    cleanName nm = case nm of
-      MN n _     => pure (UN $ mkUserName n) -- this may be "_"
      PV n _     => pure n
-      DN n _     => pure (UN $ mkUserName n) -- this may be "_"
-      NS _ n     => cleanName n
+      -- Some of these may be "_" so we use `mkUserName`
+      MN n _     => pure (UN $ mkUserName n)
+      DN n _     => pure (UN $ mkUserName n)
+      -- namespaces have already been stripped in toPTerm if necessary
+      NS ns n    => NS ns <$> cleanName n
      Nested _ n => cleanName n
      UN n       => pure (UN n)
      _          => UN . mkUserName <$> prettyName nm
--- a/src/Idris/SetOptions.idr
+++ b/src/Idris/SetOptions.idr
@ -385,6 +385,14 @@ preOptions (Logging n :: opts)
 preOptions (ConsoleWidth n :: opts)
    = do setConsoleWidth n
         preOptions opts
+preOptions (ShowMachineNames :: opts)
+    = do pp <- getPPrint
+         setPPrint ({ showMachineNames := True } pp)
+         preOptions opts
+preOptions (ShowNamespaces :: opts)
+    = do pp <- getPPrint
+         setPPrint ({ fullNamespace := True } pp)
+         preOptions opts
 preOptions (Color b :: opts)
    = do setColor b
         preOptions opts
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@ -562,6 +562,7 @@ public export
 data REPLOpt : Type where
     ShowImplicits : Bool -> REPLOpt
     ShowNamespace : Bool -> REPLOpt
+     ShowMachineNames : Bool -> REPLOpt
     ShowTypes : Bool -> REPLOpt
     EvalMode : REPLEval -> REPLOpt
     Editor : String -> REPLOpt
@ -573,6 +574,7 @@ export
 Show REPLOpt where
  show (ShowImplicits impl) = "showimplicits = " ++ show impl
  show (ShowNamespace ns) = "shownamespace = " ++ show ns
+  show (ShowMachineNames mn) = "showmachinenames = " ++ show mn
  show (ShowTypes typs) = "showtypes = " ++ show typs
  show (EvalMode mod) = "eval = " ++ show mod
  show (Editor editor) = "editor = " ++ show editor
@ -582,14 +584,15 @@ Show REPLOpt where

 export
 Pretty Void REPLOpt where
-  pretty (ShowImplicits impl) = pretty "showimplicits" <++> equals <++> pretty (show impl)
-  pretty (ShowNamespace ns) = pretty "shownamespace" <++> equals <++> pretty (show ns)
-  pretty (ShowTypes typs) = pretty "showtypes" <++> equals <++> pretty (show typs)
-  pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod
-  pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor
-  pretty (CG str) = pretty "cg" <++> equals <++> pretty str
-  pretty (Profile p) = pretty "profile" <++> equals <++> pretty (show p)
-  pretty (EvalTiming p) = pretty "evaltiming" <++> equals <++> pretty (show p)
+  pretty (ShowImplicits impl) = "showimplicits" <++> equals <++> pretty (show impl)
+  pretty (ShowNamespace ns) = "shownamespace" <++> equals <++> pretty (show ns)
+  pretty (ShowMachineNames mn) = "showmachinenames" <++> equals <++> pretty (show mn)
+  pretty (ShowTypes typs) = "showtypes" <++> equals <++> pretty (show typs)
+  pretty (EvalMode mod) = "eval" <++> equals <++> pretty mod
+  pretty (Editor editor) = "editor" <++> equals <++> pretty editor
+  pretty (CG str) = "cg" <++> equals <++> pretty str
+  pretty (Profile p) = "profile" <++> equals <++> pretty (show p)
+  pretty (EvalTiming p) = "evaltiming" <++> equals <++> pretty (show p)

 public export
 data EditCmd : Type where
--- a/src/Idris/Syntax/Traversals.idr
+++ b/src/Idris/Syntax/Traversals.idr
@ -23,9 +23,9 @@ mapPTermM f = goPTerm where
               <*> goPTerm argTy
               <*> goPTerm retTy
      >>= f
-    goPTerm (PLam fc x info z argTy scope) =
+    goPTerm (PLam fc x info pat argTy scope) =
      PLam fc x <$> goPiInfo info
-                <*> pure z
+                <*> goPTerm pat
                <*> goPTerm argTy
                <*> goPTerm scope
      >>= f
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@ -2,6 +2,7 @@ module TTImp.ProcessDef

 import Core.Case.CaseBuilder
 import Core.Case.CaseTree
+import Core.Case.CaseTree.Pretty
 import Core.Context
 import Core.Context.Log
 import Core.Core
@ -804,11 +805,13 @@ mkRunTime fc n
                              _ => clauses_init

           (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses
-           logC "compile.casetree" 5 $ pure $ unlines
-             [ show cov ++ ":"
-             , "Runtime tree for " ++ show (fullname gdef) ++ ":"
-             , show (indent 2 $ pretty !(toFullNames tree_rt))
-             ]
+           logC "compile.casetree" 5 $ do
+             tree_rt <- toFullNames tree_rt
+             pure $ unlines
+               [ show cov ++ ":"
+               , "Runtime tree for " ++ show (fullname gdef) ++ ":"
+               , show (indent 2 $ prettyTree tree_rt)
+               ]
           log "compile.casetree" 10 $ show tree_rt
           log "compile.casetree.measure" 15 $ show (measure tree_rt)

--- a/tests/Main.idr
+++ b/tests/Main.idr
@ -47,6 +47,10 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
       "interpolation001", "interpolation002", "interpolation003",
       "interpolation004"]

+idrisTestsDebug : TestPool
+idrisTestsDebug = MkTestPool "Debug features" [] Nothing
+      ["debug001"]
+
 idrisTestsCoverage : TestPool
 idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
       -- Coverage checking
@ -96,7 +100,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
       "interactive029", "interactive030", "interactive031", "interactive032",
       "interactive033", "interactive034", "interactive035", "interactive036",
       "interactive037", "interactive038", "interactive039", "interactive040",
-       "interactive041"]
+       "interactive041", "interactive042"]

 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing
@ -362,6 +366,7 @@ main = runner $
  , testPaths "idris2" idrisTestsSchemeEval
  , testPaths "idris2" idrisTestsReflection
  , testPaths "idris2" idrisTestsWith
+  , testPaths "idris2" idrisTestsDebug
  , testPaths "idris2" idrisTests
  , !typeddTests
  , !ideModeTests
--- a/tests/idris2/basic023/expected
+++ b/tests/idris2/basic023/expected
@ -3,7 +3,7 @@ Main> Main.Dict : (a -> a -> Bool) -> Type -> Type
 Main> Main.MkDict : (eq : (a -> a -> Bool)) -> List (a, b) -> Dict eq b
 Main> Main.lookup : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
 Main> Main.lookupK : (eq : (a -> a -> Bool)) -> a -> Dict eq b -> Maybe b
-Main> MkDict (\{arg:0}, {arg:1} => intToBool (prim__eq_Int arg arg)) [(0, "foo"), (1, "bar")]
+Main> MkDict (\arg, arg => intToBool (prim__eq_Int arg arg)) [(0, "foo"), (1, "bar")]
 Main> Just "bar"
 Main> Nothing
 Main> Bye for now!
--- a/tests/idris2/coverage018/expected
+++ b/tests/idris2/coverage018/expected
@ -1,20 +1,20 @@
 1/1: Building Issue1831_1 (Issue1831_1.idr)
 Issue1831_1> Issue1831_1.test2
 Arguments [{arg:0}]
-Compile time tree: case {arg:0} : [__] of
-  Prelude.Types.S {e:0} => case {e:0} : [__] of
-    Prelude.Types.S {e:1} => case {e:1} : [__] of
-      Prelude.Types.Z => Prelude.Basics.True
-      _ => Prelude.Basics.False
-    _ => Prelude.Basics.False
-  _ => Prelude.Basics.False
-Compiled: \ {arg:0} => case !{arg:0} of
+Compile time tree: case {arg:0} of
+  S {e:0} => case {e:0} of
+    S {e:1} => case {e:1} of
+      Z => True
+      _ => False
+    _ => False
+  _ => False
+Compiled: \ {arg:0} => case {arg:0} of
  { 0 => 0
-  ; _ => let {e:0} = !{arg:0} - 1 in
-         case !{e:0} of
+  ; _ => let {e:0} = {arg:0} - 1 in
+         case {e:0} of
           { 0 => 0
-           ; _ => let {e:1} = !{e:0} - 1 in
-                  case !{e:1} of
+           ; _ => let {e:1} = {e:0} - 1 in
+                  case {e:1} of
                    { 0 => 1
                    ; _ => 0
                    }
@ -27,20 +27,20 @@ Bye for now!
 1/1: Building Issue1831_2 (Issue1831_2.idr)
 Issue1831_2> Issue1831_2.test2
 Arguments [{arg:0}]
-Compile time tree: case {arg:0} : [__] of
-  Prelude.Types.S {e:0} => case {e:0} : [__] of
-    Prelude.Types.S {e:1} => case {e:1} : [__] of
-      Prelude.Types.Z => Prelude.Basics.True
-      _ => Prelude.Basics.False
-    _ => Prelude.Basics.False
-  _ => Prelude.Basics.False
-Compiled: \ {arg:0} => case !{arg:0} of
+Compile time tree: case {arg:0} of
+  S {e:0} => case {e:0} of
+    S {e:1} => case {e:1} of
+      Z => True
+      _ => False
+    _ => False
+  _ => False
+Compiled: \ {arg:0} => case {arg:0} of
  { 0 => 0
-  ; _ => let {e:0} = !{arg:0} - 1 in
-         case !{e:0} of
+  ; _ => let {e:0} = {arg:0} - 1 in
+         case {e:0} of
           { 0 => 0
-           ; _ => let {e:1} = !{e:0} - 1 in
-                  case !{e:1} of
+           ; _ => let {e:1} = {e:0} - 1 in
+                  case {e:1} of
                    { 0 => 1
                    ; _ => 0
                    }
--- a/tests/idris2/debug001/TypePat.idr
+++ b/tests/idris2/debug001/TypePat.idr
@ -0,0 +1,7 @@
+isNat : Type -> Bool
+isNat Nat = True
+isNat _ = False
+
+isInt32 : Type -> Bool
+isInt32 Int32 = True
+isInt32 _ = False
--- a/tests/idris2/debug001/expected
+++ b/tests/idris2/debug001/expected
@ -0,0 +1,81 @@
+1/1: Building TypePat (TypePat.idr)
+Main> Main.isNat
+Arguments [{arg:0}]
+Compile time tree: case {arg:0} of
+  Nat => True
+  _ => False
+Compiled: \ {arg:0} => case {arg:0} of
+  { Prelude.Types.Nat [tycon] => 1
+  ; _ => 0
+  }
+Refers to: Prelude.Basics.True, Prelude.Basics.False
+Flags: allguarded, covering
+Main> Main.isInt32
+Arguments [{arg:0}]
+Compile time tree: case {arg:0} of
+  Int32 => True
+  _ => False
+Compiled: \ {arg:0} => case {arg:0} of
+  { Int32 [tycon] => 1
+  ; _ => 0
+  }
+Refers to: Prelude.Basics.True, Prelude.Basics.False
+Flags: allguarded, covering
+Main> Prelude.Types.plus
+Arguments [{arg:0}, {arg:1}]
+Compile time tree: case {arg:0} of
+  Z => {arg:1}
+  S {e:0} => S (plus {e:0} {arg:1})
+Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
+  { 0 => {arg:1}
+  ; _ => let {e:0} = {arg:0} - 1 in
+         ({e:0} + {arg:1}) + 1
+  }
+Refers to: Prelude.Types.plus, Prelude.Types.S
+Flags: total
+Size change: Prelude.Types.plus: [Just (0, Smaller), Just (1, Same)]
+Main> Prelude.Types.minus
+Arguments [{arg:0}, {arg:1}]
+Compile time tree: case {arg:0} of
+  Z => 0
+  _ => case {arg:1} of
+    Z => {arg:0}
+    _ => case {arg:0} of
+      S {e:0} => case {arg:1} of
+        S {e:1} => minus {e:0} {e:1}
+Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
+  { 0 => 0
+  ; _ => case {arg:1} of
+           { 0 => {arg:0}
+           ; _ => case {arg:0} of
+                    { 0 => crash "Nat case not covered"
+                    ; _ => let {e:0} = {arg:0} - 1 in
+                           case {arg:1} of
+                             { 0 => crash "Nat case not covered"
+                             ; _ => let {e:1} = {arg:1} - 1 in
+                                    Prelude.Types.prim__integerToNat ({e:0} - {e:1})
+                             }
+                    }
+           }
+  }
+Refers to: Prelude.Types.minus, Prelude.Types.Z
+Refers to (runtime): Prelude.Types.prim__integerToNat
+Flags: total
+Size change: Prelude.Types.minus: [Just (0, Smaller), Just (1, Smaller)]
+Main> Prelude.Types.SnocList.filter
+Arguments [{arg:0}, {arg:1}, {arg:2}]
+Compile time tree: case {arg:2} of
+  Lin {e:0} => [<]
+  (:<) {e:1} {e:2} {e:3} => let rest = filter {arg:1} {e:2} in if {arg:1} {e:3} then rest :< x else rest
+Erasable args: [0]
+Inferrable args: [0]
+Compiled: \ {arg:1}, {arg:2} => case {arg:2} of
+  { Prelude.Basics.Lin {tag = 0} [nil] => Prelude.Basics.Lin {tag = 0} [nil]
+  ; Prelude.Basics.(:<) {tag = 1} [cons] {e:2} {e:3} => let rest = Prelude.Types.SnocList.filter {arg:1} {e:2} incase {arg:1} {e:3} of  { 1 => Prelude.Basics.(:<) {tag = 1} [cons] rest {e:3}; 0 => rest}
+  }
+Refers to: Prelude.Basics.SnocList, Prelude.Basics.Lin, Prelude.Types.SnocList.case block in filter, Prelude.Types.SnocList.filter
+Refers to (runtime): Prelude.Basics.Lin, Prelude.Basics.(:<), Prelude.Types.SnocList.filter
+Flags: total
+Size change: Prelude.Types.SnocList.filter: [Just (0, Same), Just (1, Same), Just (2, Smaller)]
+Main> 
+Bye for now!
--- a/tests/idris2/debug001/input
+++ b/tests/idris2/debug001/input
@ -0,0 +1,6 @@
+:di isNat
+:di isInt32
+:di plus
+:di minus
+:di SnocList.filter
+:q
--- a/tests/idris2/debug001/run
+++ b/tests/idris2/debug001/run
@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner TypePat.idr < input
--- a/tests/idris2/docs004/expected
+++ b/tests/idris2/docs004/expected
@ -81,7 +81,7 @@ shiftR : Integer -> Index -> Integer
 shiftR x = prim__shr_Integer x . natToInteger

 bit : Index -> Integer
-bit = \{arg:0} => 1 `shiftL` arg
+bit = \arg => 1 `shiftL` arg

 zeroBits : Integer
 zeroBits = 0
--- a/tests/idris2/inlining001/expected
+++ b/tests/idris2/inlining001/expected
@ -1,39 +1,39 @@
 1/1: Building Inlining (Inlining.idr)
 Main> Main.leaveAlone
 Arguments [{arg:0}]
-Compile time tree: (Prelude.Types.String.++ {arg:0}[0] "!")
-Compiled: \ {arg:0} => !{arg:0} ++ "!"
+Compile time tree: {arg:0} ++ "!"
+Compiled: \ {arg:0} => {arg:0} ++ "!"
 Refers to: Prelude.Types.String.(++)
 Flags: covering
 Size change: Prelude.Types.String.(++): [Just (0, Same), Nothing]
 Main> Main.forceInline
 Arguments [{arg:0}]
-Compile time tree: (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 {arg:0}[0] (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))))))))))
-Compiled: \ {arg:0} => !{arg:0} + 10
+Compile time tree: {arg:0} + 10
+Compiled: \ {arg:0} => {arg:0} + 10
 Refers to: Prelude.Types.Num implementation at Prelude.Types:66:1--71:33, Prelude.Types.Z, Prelude.Types.S, Prelude.Types.Nat, Prelude.Num.(+)
 Flags: covering, inline
 Size change: Prelude.Num.(+): [Nothing, Nothing, Just (0, Same), Nothing], Prelude.Types.Num implementation at Prelude.Types:66:1--71:33: []
 Main> Main.forceNoInline
 Arguments []
-Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))))))))))
+Compile time tree: 10
 Compiled: 10
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering, noinline
 Main> Main.heuristicPublicInline
 Arguments []
-Compile time tree: (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))
+Compile time tree: 2
 Compiled: 2
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: inline, allguarded, covering
 Main> Main.exportedForced
 Arguments []
-Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))))))))))))))))))))))))))))))))
+Compile time tree: 33
 Compiled: 33
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering, inline
 Main> Main.exportedUnforced
 Arguments []
-Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+Compile time tree: 66
 Compiled: 66
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering
--- a/tests/idris2/interactive042/Issue35-2.idr
+++ b/tests/idris2/interactive042/Issue35-2.idr
@ -0,0 +1,4 @@
+f : { a, b : Type } -> Either a b -> Either b a
+f {a=b} x = x
+f (Right x) = Left x
+f (Left x) = Right x
--- a/tests/idris2/interactive042/Issue35.idr
+++ b/tests/idris2/interactive042/Issue35.idr
@ -0,0 +1,10 @@
+test : {a : Nat} -> (b : Nat) -> a === b -> Nat
+test a eq = ?a
+
+data Vect : Nat -> Type -> Type where
+  Nil : Vect 0 a
+  (::) : a -> Vect n a -> Vect (S n) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = ?help
--- a/tests/idris2/interactive042/expected
+++ b/tests/idris2/interactive042/expected
@ -0,0 +1,63 @@
+1/1: Building Issue35 (Issue35.idr)
+Main>    a : Nat
+   eq : a = a
+------------------------------
+a : Nat
+Main>  0 m : Nat
+ 0 a : Type
+   x : a
+   xs : Vect n a
+   ys : Vect m a
+ 0 n : Nat
+------------------------------
+help : Vect (S (plus n m)) a
+Main> Main>    a : Nat
+   eq : {a:827} = a
+------------------------------
+a : Nat
+Main>  0 m : Nat
+ 0 a : Type
+   x : a
+   xs : Vect {n:876} a
+   ys : Vect m a
+ 0 n : Nat
+------------------------------
+help : Vect (S (plus {n:876} m)) a
+Main> 
+Bye for now!
+1/1: Building Issue35-2 (Issue35-2.idr)
+Error: While processing right hand side of f. When unifying:
+    Either b b
+and:
+    Either b b
+Mismatch between: b (implicitly bound at Issue35-2:2:1--2:14) and b.
+
+Issue35-2:2:13--2:14
+ 1 | f : { a, b : Type } -> Either a b -> Either b a
+ 2 | f {a=b} x = x
+                 ^
+
+1/1: Building Issue35-2 (Issue35-2.idr)
+Error: While processing right hand side of f. When unifying:
+    Either b {b:826}
+and:
+    Either {b:826} b
+Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b.
+
+Issue35-2:2:13--2:14
+ 1 | f : { a, b : Type } -> Either a b -> Either b a
+ 2 | f {a=b} x = x
+                 ^
+
+1/1: Building Issue35-2 (Issue35-2.idr)
+Error: While processing right hand side of f. When unifying:
+    Prelude.Either b {b:826}
+and:
+    Prelude.Either {b:826} b
+Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b.
+
+Issue35-2:2:13--2:14
+ 1 | f : { a, b : Type } -> Either a b -> Either b a
+ 2 | f {a=b} x = x
+                 ^
+
--- a/tests/idris2/interactive042/input
+++ b/tests/idris2/interactive042/input
@ -0,0 +1,6 @@
+:t a
+:t help
+:set showmachinenames
+:t a
+:t help
+:q
--- a/tests/idris2/interactive042/run
+++ b/tests/idris2/interactive042/run
@ -0,0 +1,6 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner Issue35.idr < input
+$1 --no-color --console-width 0 --no-banner --check Issue35-2.idr || true
+$1 --no-color --console-width 0 --no-banner --show-machine-names --check Issue35-2.idr || true
+$1 --no-color --console-width 0 --no-banner --show-namespaces --show-machine-names --check Issue35-2.idr || true
--- a/tests/idris2/reg042/expected
+++ b/tests/idris2/reg042/expected
@ -1,38 +1,38 @@
 1/1: Building NatOpts (NatOpts.idr)
 Main> Main.doPlus
 Arguments [{arg:0}, {arg:1}]
-Compile time tree: (Prelude.Types.plus {arg:0}[0] {arg:1}[1])
-Compiled: \ {arg:0}, {arg:1} => !{arg:0} + !{arg:1}
+Compile time tree: plus {arg:0} {arg:1}
+Compiled: \ {arg:0}, {arg:1} => {arg:0} + {arg:1}
 Refers to: Prelude.Types.plus
 Flags: covering
 Size change: Prelude.Types.plus: [Just (0, Same), Just (1, Same)]
 Main> Main.doMinus
 Arguments [{arg:0}, {arg:1}]
-Compile time tree: (Prelude.Types.minus {arg:0}[0] {arg:1}[1])
-Compiled: \ {arg:0}, {arg:1} => Prelude.Types.prim__integerToNat (!{arg:0} - !{arg:1})
+Compile time tree: minus {arg:0} {arg:1}
+Compiled: \ {arg:0}, {arg:1} => Prelude.Types.prim__integerToNat ({arg:0} - {arg:1})
 Refers to: Prelude.Types.minus
 Refers to (runtime): Prelude.Types.prim__integerToNat
 Flags: covering
 Size change: Prelude.Types.minus: [Just (0, Same), Just (1, Same)]
 Main> Main.doMult
 Arguments [{arg:0}, {arg:1}]
-Compile time tree: (Prelude.Types.mult {arg:0}[0] {arg:1}[1])
-Compiled: \ {arg:0}, {arg:1} => !{arg:0} * !{arg:1}
+Compile time tree: mult {arg:0} {arg:1}
+Compiled: \ {arg:0}, {arg:1} => {arg:0} * {arg:1}
 Refers to: Prelude.Types.mult
 Flags: covering
 Size change: Prelude.Types.mult: [Just (0, Same), Just (1, Same)]
 Main> Main.doCompare
 Arguments [{arg:0}, {arg:1}]
-Compile time tree: (Prelude.Types.compareNat {arg:0}[0] {arg:1}[1])
-Compiled: \ {arg:0}, {arg:1} => Prelude.EqOrd.compare !{arg:0} !{arg:1}
+Compile time tree: compareNat {arg:0} {arg:1}
+Compiled: \ {arg:0}, {arg:1} => Prelude.EqOrd.compare {arg:0} {arg:1}
 Refers to: Prelude.Types.compareNat
 Refers to (runtime): Prelude.EqOrd.compare
 Flags: covering
 Size change: Prelude.Types.compareNat: [Just (0, Same), Just (1, Same)]
 Main> Main.doEqual
 Arguments [{arg:0}, {arg:1}]
-Compile time tree: (Prelude.Types.equalNat {arg:0}[0] {arg:1}[1])
-Compiled: \ {arg:0}, {arg:1} => !{arg:0} == !{arg:1}
+Compile time tree: equalNat {arg:0} {arg:1}
+Compiled: \ {arg:0}, {arg:1} => {arg:0} == {arg:1}
 Refers to: Prelude.Types.equalNat
 Flags: covering
 Size change: Prelude.Types.equalNat: [Just (0, Same), Just (1, Same)]
--- a/tests/idris2/schemeeval003/expected
+++ b/tests/idris2/schemeeval003/expected
@ -1,3 +1,3 @@
-Main> [scheme] Main> 1 :: Delay (countFrom (1 + 1) (\{arg:0} => prim__add_Integer 1 arg))
+Main> [scheme] Main> 1 :: Delay (countFrom (1 + 1) (\arg => prim__add_Integer 1 arg))
 [scheme] Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
 [scheme] Main> Bye for now!
--- a/tests/idris2/with003/expected
+++ b/tests/idris2/with003/expected
@ -1,7 +1,7 @@
 1/1: Building Main (Main.idr)
 Main> Error: Ambiguous elaboration. Possible results:
-    Main.myPrintLn "foo" Prelude.(>>) Delay (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\{arg:0} => {arg:0} Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo")))
-    Main.myPrintLn "foo" Main.Other.(>>) (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\{arg:0} => {arg:0} Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo")))
+    Main.myPrintLn "foo" Prelude.(>>) Delay (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\arg => arg Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo")))
+    Main.myPrintLn "foo" Main.Other.(>>) (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\arg => arg Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo")))

 (Interactive):1:4--1:19
 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"