- T1 { f :: a } :: T [a]
- T2 { f :: a, y :: b } :: T [a]
-and now the selector takes that type as its argument:
- f :: forall a. T [a] -> a
- f t = case t of
- T1 { f = v } -> v
- T2 { f = v } -> v
+ T1 { f :: Maybe a } :: T [a]
+ T2 { f :: Maybe a, y :: b } :: T [a]
+
+and now the selector takes that result type as its argument:
+ f :: forall a. T [a] -> Maybe a
+
+Details: the "real" types of T1,T2 are:
+ T1 :: forall r a. (r~[a]) => a -> T r
+ T2 :: forall r a b. (r~[a]) => a -> b -> T r
+
+So the selector loooks like this:
+ f :: forall a. T [a] -> Maybe a
+ f (a:*) (t:T [a])
+ = case t of
+ T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
+ T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
+