Commit be1ca0e4 authored by Ryan Scott's avatar Ryan Scott
Browse files

Add regression test for #14040

This adds a regression test for the original program in #14040.

This does not fix #14040 entirely, though, as the program in
https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2 still
panics, so there is more work to be done there.
parent 9d299253
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T14040a where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type -> Type where
WeirdNil :: WeirdList a
WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs
-> p _ (WeirdCons x xs))
-> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
T14040a.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p x0 w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x
-> Sing xs
-> p (WeirdList z1) w1 xs
-> p z1 w2 ('WeirdCons x xs))
-> p a w3 wl’
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
......@@ -64,4 +64,5 @@ test('PatBind3', normal, compile_fail, [''])
test('T12039', normal, compile_fail, [''])
test('T12634', normal, compile_fail, [''])
test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
test('T14040a', normal, compile_fail, [''])
test('T14449', normal, compile_fail, [''])
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