Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / partial-sigs / should_compile / T15039a.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PartialTypeSignatures #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE PolyKinds #-}
6 {-# LANGUAGE TypeOperators #-}
7 {-# OPTIONS_GHC -fdefer-type-errors #-}
8 module T15039a where
9
10 import Data.Coerce
11 import Data.Kind
12 import Data.Type.Coercion
13 import Data.Type.Equality
14
15 data Dict :: Constraint -> Type where
16 Dict :: c => Dict c
17
18 ex1 :: Dict ((a :: Type) ~ (b :: Type)) -> ()
19 ex1 (Dict :: _) = ()
20
21 ex2 :: Dict ((a :: Type) ~~ (b :: Type)) -> ()
22 ex2 (Dict :: _) = ()
23
24 ex3 :: Dict ((a :: Type) ~~ (b :: k)) -> ()
25 ex3 (Dict :: _) = ()
26
27 -- Don't know how to make GHC print an unlifted, nominal equality in an error
28 -- message.
29 --
30 -- ex4, ex5 :: ???
31
32 ex6 :: Dict (Coercible (a :: Type) (b :: Type)) -> ()
33 ex6 (Dict :: _) = ()
34
35 ex7 :: _ => Coercion (a :: Type) (b :: Type)
36 ex7 = Coercion
37
38 -- Don't know how to make GHC print an unlifted, heterogeneous,
39 -- representational equality in an error message.
40 --
41 -- ex8 :: ???