Commit 376902ee authored by simonpj's avatar simonpj
Browse files

Track change in record syntax for GADTs

parent 79b7a9c6
......@@ -5,9 +5,9 @@
module Main where
data T a where
T1 { x :: a, y :: b } :: T (a,b)
T2 { x :: a } :: T (a,b)
T3 { z :: Int } :: T Bool
T1 :: { x :: a, y :: b } -> T (a,b)
T2 :: { x :: a } -> T (a,b)
T3 :: { z :: Int } -> T Bool
f xv yv = T1 { x = xv, y = yv }
......
......@@ -7,15 +7,15 @@ module Rec where
----------------- Existential
data S a where
S1 { fs1 :: a, fs2 :: b } :: S a
S2 { fs1 :: a } :: S a
S1 :: { fs1 :: a, fs2 :: b } -> S a
S2 :: { fs1 :: a } -> S a
updS s x = s { fs1=x }
------------------ GADT
data T a b where
T1 { ft1 :: a, ft2 :: c, ft3 :: d } :: T a Int
T2 { ft1 :: a, ft3 :: c } :: T a Int
T1 :: { ft1 :: a, ft2 :: c, ft3 :: d } -> T a Int
T2 :: { ft1 :: a, ft3 :: c } -> T a Int
T3 :: T Int b
f :: T a1 b -> a2 -> T a2 b
......@@ -24,7 +24,7 @@ f x v = x { ft1 = v }
------------------ Type family
data family R a
data instance R (a,b) where
R1 { fr1 :: a, fr2 :: b, fr3 :: c } :: R (a,b)
R2 { fr1 :: a, fr3 :: c } :: R (a,b)
R1 :: { fr1 :: a, fr2 :: b, fr3 :: c } -> R (a,b)
R2 :: { fr1 :: a, fr3 :: c } -> R (a,b)
updR r x = r { fr1=x }
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment