blob: 789798b3708ea14b06106886343fe771cfdb2901 (
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
42
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnicodeSyntax #-}
module T16326_Compile1 where
import Data.Kind
type DApply a (b :: a -> Type) (f :: forall (x :: a) -> b x) (x :: a) =
f x
type DComp a
(b :: a -> Type)
(c :: forall (x :: a). b x -> Type)
(f :: forall (x :: a). forall (y :: b x) -> c y)
(g :: forall (x :: a) -> b x)
(x :: a) =
f (g x)
-- Ensure that ElimList has a CUSK, beuas it is
-- is used polymorphically its RHS (c.f. Trac #16344)
type family ElimList (a :: Type)
(p :: [a] -> Type)
(s :: [a])
(pNil :: p '[])
(pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs))
:: p s where
forall a p pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)).
ElimList a p '[] pNil pCons =
pNil
forall a p x xs pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)).
ElimList a p (x:xs) pNil pCons =
pCons x xs (ElimList a p xs pNil pCons)
data Proxy' :: forall k -> k -> Type where
MkProxy' :: forall k (a :: k). Proxy' k a
type family Proxy2' ∷ ∀ k → k → Type where
Proxy2' = Proxy'
|
