blob: 5a81558badc8ed58675cd4bac4668bdfd442aa50 (
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
|
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
module T15772 where
import Data.Kind
data NP (f :: Type -> Type) (xs :: [Type])
type family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a
uncurry_NP = undefined
fun_NP :: NP Id xs -> ()
fun_NP = undefined
newtype Id a = MkId a
-- Bizarrely: uncommenting this allows the program to type-check in GHC 8.8
-- It should type-check without it.
-- test1 :: ()
-- test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
|
