blob: 6283b18071dc857e3e7f0033e967fab2882b3072 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
module T2102 where
type family Cat ts0 ts
type instance Cat () ts' = ts'
type instance Cat (s, ts) ts' = (s, Cat ts ts')
class (Cat ts () ~ ts) => Valid ts
instance Valid () -- compiles OK
instance Valid ts => Valid (s, ts) -- fails to compile
-- need to prove Cat (s, ts) () ~ (s, Cat ts ())
-- for the superclass of class Valid.
-- (1) From Valid ts: Cat ts () ~ ts
-- (2) Therefore: (s, Cat ts ()) ~ (s, ts)
coerce :: forall f ts. Valid ts => f (Cat ts ()) -> f ts
coerce x = x
|
