diff options
Diffstat (limited to 'testsuite')
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/T17923.hs | 44 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 |
2 files changed, 45 insertions, 0 deletions
diff --git a/testsuite/tests/indexed-types/should_compile/T17923.hs b/testsuite/tests/indexed-types/should_compile/T17923.hs new file mode 100644 index 0000000000..8c34024864 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T17923.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wall #-} +module Bug where + +import Data.Kind + +-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2) +type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2) +singFun2 :: forall f. SingFunction2 f -> Sing f +singFun2 f = SLambda (\x -> SLambda (f x)) + +type family Sing :: k -> Type +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type family Apply (f :: a ~> b) (x :: a) :: b +data Sym4 a +data Sym3 a + +type instance Apply Sym3 _ = Sym4 + +newtype SLambda (f :: k1 ~> k2) = + SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } +type instance Sing = SLambda + +und :: a +und = undefined + +data E +data ShowCharSym0 :: E ~> E ~> E + +sShow_tuple :: SLambda Sym4 +sShow_tuple + = applySing (singFun2 @Sym3 und) + (und (singFun2 @Sym3 + (und (applySing (singFun2 @Sym3 und) + (applySing (singFun2 @ShowCharSym0 und) und))))) diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 8bda294207..ccca063fd2 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -294,3 +294,4 @@ test('T16828', normal, compile, ['']) test('T17008b', normal, compile, ['']) test('T17056', normal, compile, ['']) test('T17405', normal, multimod_compile, ['T17405c', '-v0']) +test('T17923', normal, compile, ['']) |