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