Update Trac ticket URLs to point to GitLab
[ghc.git] / testsuite / tests / gadt / karl2.hs
1 {-# LANGUAGE GADTs, KindSignatures #-}
2
3 module Expr0 where
4
5 -- See #301
6 -- This one *does* use GADTs (Fct)
7
8 import Data.Kind (Type)
9
10 data Expr :: Type -> Type where
11 Const :: Show a => a -> Expr a
12 Apply :: Fct a b -> Expr a -> Expr b
13
14 data Fct :: Type -> Type -> Type where
15 Succ :: Fct Int Int
16 EqZero :: Fct Int Bool
17 Add :: Fct Int (Int -> Int)
18
19 ------------------------------
20 e1 :: Expr Int
21 e1 = Apply Succ (Const 41)
22
23 e2 :: Expr Bool
24 e2 = Apply EqZero e1
25
26 e3 :: Expr (Int -> Int)
27 e3 = Apply Add e1
28
29 ------------------------------
30 eval :: Expr a -> a
31 eval (Const c) = c
32 eval (Apply f a) = evalFct f $ eval a
33
34 evalFct :: Fct a b -> a -> b
35 evalFct Succ = succ
36 evalFct EqZero = (0 ==)
37 evalFct Add = (+)
38
39
40 {- Up to here, everything works nicely:
41
42 \begin{verbatim}
43 *Expr0> eval e1
44 42
45 *Expr0> eval e2
46 False
47 *Expr0> eval e3 5
48 47
49 \end{verbatim}
50
51 But let us now try to define a |Show| instance.
52 For |Fct|, this is not a problem:
53 -}
54
55 instance Show (Fct a b) where
56 show Succ = "S"
57 show EqZero = "isZero"
58 show Add = "add"
59
60 showsExpr :: Expr a -> ShowS
61 showsExpr (Const c) = shows c
62 showsExpr (Apply f a) =
63 ('(' :) . shows f . (' ' :) . showsExpr a . (')' :)
64
65 instance Show (Expr a) where
66 showsPrec _ (Const c) = shows c
67 showsPrec _ (Apply f a) =
68 ('(' :) . shows f . (' ' :) . shows a . (')' :)
69
70 {- But we used to get a complaint about the |Const| alternative (then
71 line 56) that documents that the constraint in the type of |Const|
72 must have been ignored:
73
74 \begin{verbatim}
75 No instance for (Show a)
76 arising from use of `shows' at Expr0.lhs:56:22-26
77 Probable fix: add (Show a) to the type signature(s) for `showsExpr'
78 In the definition of `showsExpr': showsExpr (Const c) = shows c
79 \end{verbatim}
80
81 But if we do that, the recursive call is of course still unsatisfied:
82 \begin{verbatim}
83 No instance for (Show a)
84 arising from use of `showsExpr' at Expr0.lhs:65:34-42
85 Probable fix: add (Show a) to the existential context for `Apply'
86 In the first argument of `(.)', namely `showsExpr a'
87 In the second argument of `(.)', namely `(showsExpr a) . ((')' :))'
88 In the second argument of `(.)', namely
89 `((' ' :)) . ((showsExpr a) . ((')' :)))'
90 \end{verbatim}
91
92 Following also the advice given in this last error message
93 actually makes GHC accept this, and then we can say:
94
95 \begin{verbatim}
96 *Expr0> showsExpr e1 ""
97 "(S 41)"
98 *Expr0> showsExpr e2 ""
99 "(isZero (S 41))"
100 \end{verbatim}
101
102 However, following this advice is counterintuitive
103 and should be unnecessary
104 since the |Show| instance for argument types
105 is only ever used in the const case.
106 We get:
107
108 \begin{verbatim}
109 *Expr0> showsExpr e3 ""
110
111 <interactive>:1:0:
112 No instance for (Show (Int -> Int))
113 arising from use of `showsExpr' at <interactive>:1:0-8
114 Probable fix: add an instance declaration for (Show (Int -> Int))
115 In the definition of `it': it = showsExpr e3 ""
116 \end{verbatim}
117
118 But of course we would expect the following:
119
120 \begin{verbatim}
121 *Expr0> showsExpr e3 ""
122 "(add (S 41))"
123 \end{verbatim}
124
125
126 \bigskip
127 The error messages are almost the same
128 if we define a |Show| instance directly
129 (line 90 was the |Const| alternative):
130
131 \begin{verbatim}
132 Could not deduce (Show a) from the context (Show (Expr a))
133 arising from use of `shows' at Expr0.lhs:90:26-30
134 Probable fix: add (Show a) to the class or instance method `showsPrec'
135 \end{verbatim}
136 -}
137
138