Don't show MN names in hole contexts

This prevents display of shadowed names from case blocks/where clauses
that are now unusable. It does mean that constraint arguments aren't
displayed, unless given an explicit name - this may not be good, since
we might want to know which constraints are in scope, so it may yet need
a little tweaking.

libs/prelude/PrimIO.idr

@@ -6,14 +6,14 @@ public export
 data IORes : Type -> Type where
      MkIORes : (result : a) -> (1 x : %World) -> IORes a
 
-export
-data IO : Type -> Type where
-     MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
-
 public export
 PrimIO : Type -> Type
 PrimIO a = (1 x : %World) -> IORes a
 
+export
+data IO : Type -> Type where
+     MkIO : (1 fn : PrimIO a) -> IO a
+
 export
 prim_io_pure : a -> PrimIO a
 prim_io_pure x = \w => MkIORes x w

src/Idris/REPL.idr

@@ -83,8 +83,7 @@ impBracket True str = "{" ++ str ++ "}"
 
 showName : Name -> Bool
 showName (UN "_") = False
-showName (MN "_" _) = False
-showName (MN "_cn" _) = False
+showName (MN _ _) = False
 showName _ = True
 
 tidy : Name -> String

tests/idris2/interactive009/expected

@@ -3,14 +3,12 @@ Main>               (y @@ res) => ?now_4
 Main>               (True @@ d) => ?now_4
               (False @@ d) => ?now_5
 Main>  0 m : Type -> Type
- 0 d : Door Closed
    x : Integer
  1 d : Door Open
  0 r : Res Bool (\r => (Door (if r then Open else Closed)))
 -------------------------------------
 now_2 : Use Many m ()
 Main>  0 m : Type -> Type
- 0 d : Door Closed
    x : Integer
  1 d : Door Closed
  0 r : Res Bool (\r => (Door (if r then Open else Closed)))

tests/idris2/interface001/expected

@@ -6,7 +6,6 @@ IFace> Bye for now!
 2/2: Building IFace1 (IFace1.idr)
 IFace1>  0 a : Type
  0 p : a -> Type
-   conArg : (DecEq a, Eq (p t))
    l' : a
    r : p l'
    r' : p l'

tests/idris2/interface003/expected

@@ -3,7 +3,6 @@ Main>  0 b : Type
  0 a' : Type
  0 a : Type
  0 m : Type -> Type
-   conArg : Monad m
    x : m a
 -------------------------------------
 foo : (a' -> m b) -> m b

tests/idris2/interface009/expected

@@ -2,7 +2,6 @@
 Main>  0 v : Type
  0 k' : Type
  0 k : Type
-   conArg : Eq k
    z : List (k', v)
    y : v
    x : k'