blob: f9d904f2a1b63f1ebf3bad95621d1aad2c3110a7 (
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
43
44
45
|
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
{-# LANGUAGE KindSignatures, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
module T13538 where
import GHC.TypeLits
import Data.Proxy
-- | Synonym for a type-level snoc (injective!)
type (ns :: [k]) +: (n :: k) = GetList1 (SinkFirst (n ': ns))
infixl 5 +:
-- | A weird data type used to make `(+:)` operation injective.
-- `List k [k]` must have at least two elements.
data List1 k = L1Single k | L1Head k [k]
-- | Sink first element of a list to the end of the list
type family SinkFirst (xs :: [k]) = (ys :: List1 k) | ys -> xs where
SinkFirst '[y] = 'L1Single y
-- SinkFirst (y ': x ': xs :: [Nat])
-- = ('L1Head x (GetList1Nat (SinkFirst (y ': xs))) :: List1 Nat)
SinkFirst (y ': x ': xs :: [k])
= ('L1Head x (GetList1 (SinkFirst (y ': xs))) :: List1 k)
type family GetList1 (ts :: List1 k) = (rs :: [k]) | rs -> ts where
GetList1 ('L1Single x) = '[x]
GetList1 ('L1Head y (x ':xs)) = y ': x ': xs
type family GetList1Nat (ts :: List1 Nat) = (rs :: [Nat]) | rs -> ts where
GetList1Nat ('L1Single x) = '[x]
GetList1Nat ('L1Head y (x ': xs)) = y ': x ': xs
type family (++) (as :: [k]) (bs :: [k]) :: [k] where
'[] ++ bs = bs
(a ': as) ++ bs = a ': (as ++ bs)
ff :: Proxy k -> Proxy (as +: k) -> Proxy (k ': bs) -> Proxy (as ++ bs)
ff _ _ _ = Proxy
yy :: Proxy '[3,7,2]
yy = ff (Proxy @5) (Proxy @'[3,7,5]) (Proxy @'[5,2])
|
