[ fix ] Data and Type Constructor tags for :di

CHANGELOG.md

@@ -42,6 +42,7 @@ This CHANGELOG describes the history of already-released versions. Please see [C
   and `Force`.
 * Adds `--no-cse` command-line option to disable common subexpression elimination
   for code generation debugging.
+* Fixes a confusion between data and type constructors in the `:di` command.
 
 ### Backend changes
 

src/Core/CompileExpr/Pretty.idr

@@ -125,7 +125,7 @@ prettyCDef (MkFun args exp) = reAnnotate Syntax $
   keyword "\\" <++> concatWith (\ x, y => x <+> keyword "," <++> y) (map prettyName args)
        <++> fatArrow <++> prettyCExp exp
 prettyCDef (MkCon mtag arity nt)
-  = vcat $ header (maybe "Data" (const "Type") mtag <++> "Constructor") :: map (indent 2)
+  = vcat $ header (maybe "Type" (const "Data") mtag <++> "Constructor") :: map (indent 2)
          ( maybe [] (\ tag => ["tag:" <++> byShow tag]) mtag ++
          [ "arity:" <++> byShow arity ] ++
            maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)

tests/idris2/basic/basic039/expected

@@ -4,7 +4,7 @@ Data constructor:
   tag: 0
   arity: 1
   newtype by: (False, 0)
-Compiled: Type Constructor:
+Compiled: Data Constructor:
   tag: 0
   arity: 1
   newtype by: 0
@@ -13,7 +13,7 @@ Main> Main.MkBar
 Data constructor:
   tag: 0
   arity: 1
-Compiled: Type Constructor:
+Compiled: Data Constructor:
   tag: 0
   arity: 1
 Flags: contype [record]

tests/idris2/repl/repl007/expected

@@ -0,0 +1,18 @@
+Main> Prelude.Basics.Bool
+Type constructor:
+  tag: 100
+  arity: 0
+  parameter positions: []
+  constructors: Prelude.Basics.False, Prelude.Basics.True
+Compiled: Type Constructor:
+  arity: 0
+Main> Prelude.Basics.True
+Data constructor:
+  tag: 1
+  arity: 0
+Compiled: Data Constructor:
+  tag: 1
+  arity: 0
+Flags: contype [enum 2]
+Main> 
+Bye for now!

tests/idris2/repl/repl007/input

@@ -0,0 +1,2 @@
+:di Bool
+:di True

tests/idris2/repl/repl007/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 < input