Commit e61900c9 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari
Browse files

Add regression test for #13538

Commit 2b64e926 (#13135) ended
up fixing #13538 as well. Let's add a regression test so that it stays
fixed.

Test Plan: make test TEST=T13538

Reviewers: austin, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13538

Differential Revision: https://phabricator.haskell.org/D3426
parent f3af0463
{-# 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])
......@@ -22,3 +22,4 @@ test('RaeJobTalk', normal, compile, [''])
test('T11635', normal, compile, [''])
test('T11719', normal, compile, [''])
test('T12442', normal, compile, [''])
test('T13538', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment