1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
{-# LANGUAGE DeriveDataTypeable,
FlexibleContexts, FlexibleInstances,
MultiParamTypeClasses,
OverlappingInstances, UndecidableInstances,
Rank2Types, KindSignatures, EmptyDataDecls #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where
class Sat a where
dict :: a -- Holds a default value
class Sat a => Data a where
gunfold :: (forall b r. Data b => (b -> r) -> r) -> a
instance (Sat [a], Data a) => Data [a] where
gunfold _ = []
class Data a => Default a where
defaultValue :: a
defaultValue = gunfold (\c -> c dict)
instance Default t => Sat t where
dict = defaultValue
instance Default a => Default [a] where
defaultValue = []
data Proposition = Prop Expression
data Expression = Conj [Expression]
instance Data Expression => Data Proposition where
gunfold k = k Prop
instance (Data [Expression],Sat Expression) => Data Expression where
-- DV: Notice what happens when we remove the Sat Expression above!
-- Everything starts working!
gunfold k = k Conj
instance Default Expression
instance Default Proposition
main :: IO ()
main = case (defaultValue :: Proposition) of
Prop exp -> case exp of
Conj _ -> putStrLn "Hurray2!"
{- Need Default Proposition
for which we have an instance
Instance
Default Proposition
needs superclass
Data Proposition
via instance dfun, needs
Data Expression
via instance dfun, needs
Sat Expression
via instance dfun, needs
Default Expression
for which we have an instance
Instance
d1: Default Expression
needs superclass [d1 = MkD d2 ..]
d2: Data Expression {superclass Sat Expression}
via instance dfun, [d2 = dfun d3 d4] needs
d3 : Sat Expression (and d4 : Data [Expression])
via instance dfun, [d3 = dfun d5] needs
d5 Default Expression
for which we have an instance [d5 = d1]
d1 = MkD d2 ..
d2 = dfun d3 d4
d3 = dfun d1
Instance
d1: Default Expression
needs superclass [d1 = MkD d2 ..]
d2: Data Expression {superclass Sat Expression d2' = sc d2 }
via instance dfun, [d2 = dfun d3 d4] needs
d3 : Sat Expression (and d4 : Data [Expression])
and we can solve: d3 = d2'... no: recursion checker will reject
-}
|
