Add location to the extra-constraints wildcard
[ghc.git] / testsuite / tests / partial-sigs / should_fail / T14040a.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE RankNTypes #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4 {-# LANGUAGE TypeApplications #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE DataKinds, PolyKinds #-}
7 module T14040a where
8
9 import Data.Kind
10
11 data family Sing (a :: k)
12
13 data WeirdList :: Type -> Type where
14 WeirdNil :: WeirdList a
15 WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
16
17 data instance Sing (z :: WeirdList a) where
18 SWeirdNil :: Sing WeirdNil
19 SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
20
21 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
22 (p :: forall (x :: Type). x -> WeirdList x -> Type).
23 Sing wl
24 -> (forall (y :: Type). p _ WeirdNil)
25 -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
26 Sing x -> Sing xs -> p _ xs
27 -> p _ (WeirdCons x xs))
28 -> p _ wl
29 elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
30 elimWeirdList (SWeirdCons (x :: Sing (x :: z))
31 (xs :: Sing (xs :: WeirdList (WeirdList z))))
32 pWeirdNil pWeirdCons
33 = pWeirdCons @z @x @xs x xs
34 (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)