Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / typecheck / should_compile / T13083.hs
1 {-# LANGUAGE TypeOperators #-}
2 {-# LANGUAGE TypeFamilies #-}
3 {-# LANGUAGE UndecidableInstances #-}
4
5 {-# OPTIONS_GHC -Wall #-}
6
7 -- | Bug(?) in Coercible constraint solving
8
9 module T13083 where
10
11 import Data.Kind
12 import GHC.Generics (Par1(..),(:*:)(..))
13 import GHC.Exts (coerce)
14
15 -- Representation as free vector space
16 type family V (a :: Type) :: Type -> Type
17
18 type instance V R = Par1
19 type instance V (a,b) = V a :*: V b
20
21 type instance V (Par1 a) = V a
22
23 data R = R
24
25 -- Linear map in row-major order
26 newtype L a b = L (V b (V a R))
27
28 -- Use coerce to drop newtype wrapper
29 bar :: L a b -> V b (V a R)
30 bar = coerce
31
32 {-
33 [W] L a b ~R V b (V a R)
34 -->
35 V b (V a R) ~R V b (V a R)
36 -}
37
38 {--------------------------------------------------------------------
39 Bug demo
40 --------------------------------------------------------------------}
41
42 -- A rejected type specialization of bar with a ~ (R,R), b ~ (Par1 R,R)
43 foo :: L (R,R) (Par1 R,R) -> V (Par1 R,R) (V (R,R) R)
44 -- foo :: L (a1,R) (Par1 b1,b2) -> V (Par1 b1,b2) (V (a1,R) R)
45 foo = coerce
46
47 {-
48 [W] L (a1,R) (Par1 b1, b2) ~R V (Par1 b1,b2) (V (a1,R) R)
49 -->
50 V (Par1 b1, b2) (V (a1,R) R) ~R same
51
52 -> (V (Par1 b1) :*: V b2) ((V a1 :*: V R) R)
53 -> (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
54
55 -->
56 L (a1,R) (Par1 b1, b2) ~R (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
57 -}
58
59 -- • Couldn't match representation of type ‘V Par1’
60 -- with that of ‘Par1’
61 -- arising from a use of ‘coerce’
62
63 -- Note that Par1 has the wrong kind (Type -> Type) for V Par1
64
65 -- Same error:
66 --
67 -- foo :: (a ~ (R,R), b ~ (Par1 R,R)) => L a b -> V b (V a R)
68
69 -- The following similar signatures work:
70
71 -- foo :: L (R,R) (R,Par1 R) -> V (R,Par1 R) (V (R,R) R)
72 -- foo :: L (Par1 R,R) (R,R) -> V (R,R) (V (Par1 R,R) R)
73
74 -- Same error:
75
76 -- -- Linear map in column-major order
77 -- newtype L a b = L (V a (V b s))
78
79 -- foo :: L (R,R) (Par1 R,R) -> V (R,R) (V (Par1 R,R) R)
80 -- foo = coerce
81