From f840d1b771be59000b478780dcfc1dfa2bfde624 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Stefan=20H=C3=B6ck?= <hock@zhaw.ch>
Date: Sat, 5 Oct 2024 09:37:26 +0200
Subject: [PATCH] [ fix ] Data and Type Constructor tags for :di (#3395)

* [ fix ] Data and Type Constructor tags for :di

* [ doc ] update changelog

* [ test ] add a test case

* [ test ] fix test output in basic039
---
 CHANGELOG.md                         |  1 +
 src/Core/CompileExpr/Pretty.idr      |  2 +-
 tests/idris2/basic/basic039/expected |  4 ++--
 tests/idris2/repl/repl007/expected   | 18 ++++++++++++++++++
 tests/idris2/repl/repl007/input      |  2 ++
 tests/idris2/repl/repl007/run        |  3 +++
 6 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/repl/repl007/expected
 create mode 100644 tests/idris2/repl/repl007/input
 create mode 100755 tests/idris2/repl/repl007/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5585c41c97..27c4d1471a 100644
--- a/CHANGELOG.md
+++ b/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
 
diff --git a/src/Core/CompileExpr/Pretty.idr b/src/Core/CompileExpr/Pretty.idr
index ba7ae1fc73..343fd3d6eb 100644
--- a/src/Core/CompileExpr/Pretty.idr
+++ b/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)
diff --git a/tests/idris2/basic/basic039/expected b/tests/idris2/basic/basic039/expected
index da0300021a..2cd0a3198c 100644
--- a/tests/idris2/basic/basic039/expected
+++ b/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]
diff --git a/tests/idris2/repl/repl007/expected b/tests/idris2/repl/repl007/expected
new file mode 100644
index 0000000000..863789e774
--- /dev/null
+++ b/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!
diff --git a/tests/idris2/repl/repl007/input b/tests/idris2/repl/repl007/input
new file mode 100644
index 0000000000..629c1f03e0
--- /dev/null
+++ b/tests/idris2/repl/repl007/input
@@ -0,0 +1,2 @@
+:di Bool
+:di True
diff --git a/tests/idris2/repl/repl007/run b/tests/idris2/repl/repl007/run
new file mode 100755
index 0000000000..404d7d47c6
--- /dev/null
+++ b/tests/idris2/repl/repl007/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 < input