blob: da3d5212cd20d303bc39e6a83cf37b331781d6d3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module T14808 where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
f :: [()] -> ECC () [] ()
f = ECC @() @[] @()
data ECC2 f a ctx where
ECC2 :: ctx => f a -> ECC2 f a ctx
f2 :: [()] -> ECC2 [] () ()
f2 = ECC2 @() @[] @()
|
