blob: 778abfa1e7cc161fa700987817b14337b8c34703 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, ConstraintKinds #-}
module T12919 where
import Data.Kind
data N = Z
data V :: N -> Type where
VZ :: V Z
type family VC (n :: N) :: Type where
VC Z = Type
type family VF (xs :: V n) (f :: VC n) :: Type where
VF VZ f = f
data Dict c where
Dict :: c => Dict c
prop :: xs ~ VZ => Dict (VF xs f ~ f)
prop = Dict
|
