blob: 50efb0db55c1bdb82266bcb0f06d183178ce6d16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T13881 where
data family Sing (a :: k)
data instance Sing (z :: [a]) where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x ': xs)
fl :: forall a (l :: [a]). Sing l -> Sing l
fl (SNil :: Sing (l :: [y])) = SNil
fl (SCons x xs) = SCons x xs
|
