From 64ad807f83ce7ce18ee4d81b932e5fe02ac72e9d Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Sat, 28 Oct 2023 15:37:13 +0300
Subject: [PATCH] [ deriving ] Try to reduce a type before searching it's
 showable

---
 libs/base/Deriving/Show.idr             |  2 ++
 tests/base/deriving_show/DeriveShow.idr | 14 ++++++++++++++
 tests/base/deriving_show/expected       |  5 +++++
 3 files changed, 21 insertions(+)

diff --git a/libs/base/Deriving/Show.idr b/libs/base/Deriving/Show.idr
index 847165843..e5dbdf881 100644
--- a/libs/base/Deriving/Show.idr
+++ b/libs/base/Deriving/Show.idr
@@ -245,6 +245,8 @@ namespace Show
                   let MW = rig
                     | _ => throwError (NotAnUnconstrainedValue rig)
 
+                  -- try to reduce the type before analysis
+                  ty <- try (check {expected=Type} ty >>= \x => quote x) (pure ty)
                   res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do
                            typeView f (paraz <>> []) ty
                   pure $ Just (showPrecFun fc mutualWith res v)
diff --git a/tests/base/deriving_show/DeriveShow.idr b/tests/base/deriving_show/DeriveShow.idr
index e20224fbf..8d87731b8 100644
--- a/tests/base/deriving_show/DeriveShow.idr
+++ b/tests/base/deriving_show/DeriveShow.idr
@@ -192,3 +192,17 @@ namespace EqMap
 
   eqMap : (eq : Eq key) => Show key => Show val => Show (EqMap key @{eq} val)
   eqMap = %runElab derive
+
+namespace Reducible
+
+  Y : Bool -> Type
+  Y True  = Bool
+  Y False = Nat
+
+  data X : Type where
+    X0 : X
+    X1 : Bool -> X
+    X2 : Y True -> Y False -> X
+
+  x : Show X
+  x = %runElab derive
diff --git a/tests/base/deriving_show/expected b/tests/base/deriving_show/expected
index ef1b1c15f..336cdc375 100644
--- a/tests/base/deriving_show/expected
+++ b/tests/base/deriving_show/expected
@@ -83,6 +83,11 @@ LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
 LOG derive.show.clauses:1: 
   showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5125} = eq} val -> String
   showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
+LOG derive.show.clauses:1: 
+  showPrecX : Prec -> X -> String
+  showPrecX d X0 = "X0"
+  showPrecX d (X1 x0) = showCon d "X1" (showArg x0)
+  showPrecX d (X2 x0 x1) = showCon d "X2" (concat ((showArg x0) :: ((showArg x1) :: Nil)))
 DeriveShow> "Lam (Call Add ((::) (Var Nothing) ((::) (Var (Just ())) Nil)))"
 DeriveShow> 
 Bye for now!