diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-12-02 10:27:47 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-12-08 15:31:41 -0500 |
commit | 62ed6957463a9c0f711ea698d7ed4371e00fb122 (patch) | |
tree | eb13107435b357117fda5e787ce4a70bd111a8f8 /testsuite/tests | |
parent | 8fac4b9333ef3607e75b4520d847054316cb8c2d (diff) | |
download | haskell-62ed6957463a9c0f711ea698d7ed4371e00fb122.tar.gz |
Fix kind inference for data types. Again.
This patch fixes several aspects of kind inference for data type
declarations, especially data /instance/ declarations
Specifically
1. In kcConDecls/kcConDecl make it clear that the tc_res_kind argument
is only used in the H98 case; and in that case there is no result
kind signature; and hence no need for the disgusting splitPiTys in
kcConDecls (now thankfully gone).
The GADT case is a bit different to before, and much nicer.
This is what fixes #18891.
See Note [kcConDecls: kind-checking data type decls]
2. Do not look at the constructor decls of a data/newtype instance
in tcDataFamInstanceHeader. See GHC.Tc.TyCl.Instance
Note [Kind inference for data family instances]. This was a
new realisation that arose when doing (1)
This causes a few knock-on effects in the tests suite, because
we require more information than before in the instance /header/.
New user-manual material about this in "Kind inference in data type
declarations" and "Kind inference for data/newtype instance
declarations".
3. Minor improvement in kcTyClDecl, combining GADT and H98 cases
4. Fix #14111 and #8707 by allowing the header of a data instance
to affect kind inferece for the the data constructor signatures;
as described at length in Note [GADT return types] in GHC.Tc.TyCl
This led to a modest refactoring of the arguments (and argument
order) of tcConDecl/tcConDecls.
5. Fix #19000 by inverting the sense of the test in new_locs
in GHC.Tc.Solver.Canonical.canDecomposableTyConAppOK.
Diffstat (limited to 'testsuite/tests')
25 files changed, 193 insertions, 49 deletions
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr index 6cdcf96369..3e3fa61a9b 100644 --- a/testsuite/tests/dependent/should_fail/T13780a.stderr +++ b/testsuite/tests/dependent/should_fail/T13780a.stderr @@ -3,7 +3,7 @@ T13780a.hs:9:40: error: • Couldn't match kind ‘a’ with ‘Bool’ Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’ ‘a’ is a rigid type variable bound by - a family instance declaration + the data constructor ‘SMkFoo’ at T13780a.hs:9:20-31 • In the second argument of ‘(~)’, namely ‘MkFoo’ In the definition of data constructor ‘SMkFoo’ diff --git a/testsuite/tests/deriving/should_compile/T11416.hs b/testsuite/tests/deriving/should_compile/T11416.hs index 6666764e3d..4ad68f5bac 100644 --- a/testsuite/tests/deriving/should_compile/T11416.hs +++ b/testsuite/tests/deriving/should_compile/T11416.hs @@ -12,9 +12,11 @@ newtype T f (a :: ConstantT Type f) = T (f a) deriving Functor data family TFam1 (f :: k1) (a :: k2) -newtype instance TFam1 f (ConstantT a f) = TFam1 (f a) +newtype instance TFam1 (f :: k -> Type) (ConstantT (a :: k) f) + = TFam1 (f a) deriving Functor data family TFam2 (f :: k1) (a :: k2) -newtype instance TFam2 f (a :: ConstantT Type f) = TFam2 (f a) +newtype instance TFam2 (f :: Type -> Type) (a :: ConstantT Type f) + = TFam2 (f a) deriving Functor diff --git a/testsuite/tests/deriving/should_compile/T9359.hs b/testsuite/tests/deriving/should_compile/T9359.hs index d541677911..a5301f7611 100644 --- a/testsuite/tests/deriving/should_compile/T9359.hs +++ b/testsuite/tests/deriving/should_compile/T9359.hs @@ -9,6 +9,5 @@ data Cmp a where deriving (Show, Eq) data family CmpInterval (a :: Cmp k) (b :: Cmp k) :: Type -data instance CmpInterval (V c) Sup = Starting c +data instance CmpInterval (V (c :: Type)) Sup = Starting c deriving( Show ) - diff --git a/testsuite/tests/gadt/SynDataRec.hs b/testsuite/tests/gadt/SynDataRec.hs new file mode 100644 index 0000000000..021ed0ba17 --- /dev/null +++ b/testsuite/tests/gadt/SynDataRec.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE KindSignatures, DataKinds, GADTs #-} + +module SynDataRec where + +-- This mutual recursion betwen a data type and +-- a type synonym is a little delicate. See +-- Note [GADT return types] in GHC.Tc.TyCl + +data Pass = Parsed | Renamed + +data GhcPass (c :: Pass) where + GhcPs :: GhcPs + GhcRn :: GhcRn + +type GhcPs = GhcPass 'Parsed +type GhcRn = GhcPass 'Renamed diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T index 3c146820ae..05ec39f18e 100644 --- a/testsuite/tests/gadt/all.T +++ b/testsuite/tests/gadt/all.T @@ -121,3 +121,4 @@ test('T15558', normal, compile, ['']) test('T16427', normal, compile_fail, ['']) test('T17423', expect_broken(17423), compile_and_run, ['']) test('T18191', normal, compile_fail, ['']) +test('SynDataRec', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_compile/T14111.hs b/testsuite/tests/indexed-types/should_compile/T14111.hs new file mode 100644 index 0000000000..d1af549187 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T14111.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE MagicHash, UnboxedSums, NoImplicitPrelude #-} +{-# LANGUAGE TypeFamilies #-} +-- {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE GADTs ,ExplicitNamespaces#-} +{-# LANGUAGE UnboxedTuples #-} + +module T14111 where + +import GHC.Exts +import GHC.Types +import Prelude (undefined) +import Data.Kind +import Data.Void + +data family Maybe(x :: TYPE (r :: RuntimeRep)) + +data instance Maybe (a :: Type ) where + MaybeSum :: (# a | (# #) #) -> Maybe a + +data instance Maybe (x :: TYPE 'UnliftedRep) where + MaybeSumU :: (# x | (# #) #) -> Maybe x diff --git a/testsuite/tests/indexed-types/should_compile/T8707.hs b/testsuite/tests/indexed-types/should_compile/T8707.hs new file mode 100644 index 0000000000..379fe068b2 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T8707.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, GADTs #-} + +module T8707 where + +import Data.Kind + +data family SingDF (a :: (k, k2 -> Type)) +data Ctor :: k -> Type + +data instance SingDF (a :: (Bool, Bool -> Type)) where + SFalse :: SingDF '(False, Ctor) diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 285619f570..469dd915df 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -300,3 +300,5 @@ test('T18809', normal, compile, ['-O']) test('CEqCanOccursCheck', normal, compile, ['']) test('GivenLoop', normal, compile, ['']) test('T18875', normal, compile, ['']) +test('T8707', normal, compile, ['-O']) +test('T14111', normal, compile, ['-O']) diff --git a/testsuite/tests/indexed-types/should_fail/T8368.stderr b/testsuite/tests/indexed-types/should_fail/T8368.stderr index 058dfb147c..8cd5e71bac 100644 --- a/testsuite/tests/indexed-types/should_fail/T8368.stderr +++ b/testsuite/tests/indexed-types/should_fail/T8368.stderr @@ -1,6 +1,5 @@ -T8368.hs:9:3: - Data constructor ‘MkFam’ returns type ‘Foo’ - instead of an instance of its parent type ‘Fam a’ - In the definition of data constructor ‘MkFam’ - In the data instance declaration for ‘Fam’ +T8368.hs:9:3: error: + • Couldn't match expected type ‘Fam a0’ with actual type ‘Foo’ + • In the result type of data constructor ‘MkFam’ + In the data instance declaration for ‘Fam’ diff --git a/testsuite/tests/indexed-types/should_fail/T8368a.stderr b/testsuite/tests/indexed-types/should_fail/T8368a.stderr index 5b20206745..a3d01dc47f 100644 --- a/testsuite/tests/indexed-types/should_fail/T8368a.stderr +++ b/testsuite/tests/indexed-types/should_fail/T8368a.stderr @@ -1,6 +1,7 @@ -T8368a.hs:7:3: - Data constructor ‘MkFam’ returns type ‘Fam Bool b’ - instead of an instance of its parent type ‘Fam Int b’ - In the definition of data constructor ‘MkFam’ - In the data instance declaration for ‘Fam’ +T8368a.hs:7:3: error: + • Couldn't match type ‘Bool’ with ‘Int’ + Expected: Fam Int b + Actual: Fam Bool b + • In the result type of data constructor ‘MkFam’ + In the data instance declaration for ‘Fam’ diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr index e081453659..723d0fcff3 100644 --- a/testsuite/tests/patsyn/should_fail/T15685.stderr +++ b/testsuite/tests/patsyn/should_fail/T15685.stderr @@ -1,13 +1,13 @@ T15685.hs:13:24: error: - • Could not deduce: a ~ [k0] - from the context: as ~ (a1 : as1) + • Could not deduce: k ~ [k0] + from the context: as ~ (a : as1) bound by a pattern with constructor: - Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]). - f a2 -> NS f (a2 : as), + Here :: forall {k} (f :: k -> *) (a :: k) (as :: [k]). + f a -> NS f (a : as), in a pattern synonym declaration at T15685.hs:13:19-26 - ‘a’ is a rigid type variable bound by + ‘k’ is a rigid type variable bound by the inferred type of HereNil :: NS f as at T15685.hs:13:9-15 Possible fix: add a type signature for ‘HereNil’ diff --git a/testsuite/tests/polykinds/T13659.stderr b/testsuite/tests/polykinds/T13659.stderr index 84e81d04c0..dad726be5f 100644 --- a/testsuite/tests/polykinds/T13659.stderr +++ b/testsuite/tests/polykinds/T13659.stderr @@ -1,6 +1,6 @@ -T13659.hs:14:27: error: - • Expected a type, but ‘a’ has kind ‘[*]’ - • In the first argument of ‘Format’, namely ‘'[Int, a]’ - In the type ‘Format '[Int, a]’ +T13659.hs:14:15: error: + • Expected kind ‘[*]’, but ‘a’ has kind ‘*’ + • In the first argument of ‘Format’, namely ‘a’ + In the type ‘Format a’ In the definition of data constructor ‘I’ diff --git a/testsuite/tests/polykinds/T16221a.stderr b/testsuite/tests/polykinds/T16221a.stderr index 5aa099b0f1..5945369a6c 100644 --- a/testsuite/tests/polykinds/T16221a.stderr +++ b/testsuite/tests/polykinds/T16221a.stderr @@ -1,7 +1,7 @@ T16221a.hs:6:49: error: - • Expected kind ‘k’, but ‘b’ has kind ‘k1’ - ‘k1’ is a rigid type variable bound by + • Expected kind ‘k’, but ‘b’ has kind ‘k2’ + ‘k2’ is a rigid type variable bound by an explicit forall k (b :: k) at T16221a.hs:6:20 ‘k’ is a rigid type variable bound by diff --git a/testsuite/tests/th/T11145.stderr b/testsuite/tests/th/T11145.stderr index 731349d908..b8c4a1c6a8 100644 --- a/testsuite/tests/th/T11145.stderr +++ b/testsuite/tests/th/T11145.stderr @@ -1,8 +1,7 @@ T11145.hs:8:1: error: - • Data constructor ‘MkFuggle’ returns type ‘Fuggle - Int (Maybe Bool)’ - instead of an instance of its parent type ‘Fuggle - Int (Maybe (a, b))’ - • In the definition of data constructor ‘MkFuggle’ + • Couldn't match type ‘Bool’ with ‘(a0, b0)’ + Expected: Fuggle Int (Maybe (a0, b0)) + Actual: Fuggle Int (Maybe Bool) + • In the result type of data constructor ‘MkFuggle’ In the data instance declaration for ‘Fuggle’ diff --git a/testsuite/tests/th/T9692.hs b/testsuite/tests/th/T9692.hs index 7f44342604..5394bea021 100644 --- a/testsuite/tests/th/T9692.hs +++ b/testsuite/tests/th/T9692.hs @@ -12,7 +12,7 @@ class C a where data F a (b :: k) :: Type instance C Int where - data F Int x = FInt x + data F Int (x :: Type) = FInt x $( do info <- qReify (mkName "F") runIO $ putStrLn $ pprint info diff --git a/testsuite/tests/typecheck/should_compile/T18891.hs b/testsuite/tests/typecheck/should_compile/T18891.hs new file mode 100644 index 0000000000..6b986ef543 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T18891.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE GADTs, UnliftedNewtypes, StandaloneKindSignatures, RankNTypes, TypeFamilies, PolyKinds #-} + +module T18891 where + +import GHC.Exts( TYPE ) + +data family T2 (a :: k) +data instance T2 a where + MkT2 :: T2 Maybe + +newtype N3 :: forall k -> TYPE k where + MkN3 :: N3 m -> N3 m + +type N4 :: forall k -> TYPE k +newtype N4 :: forall k -> TYPE k where + MkN4 :: N4 m -> N4 m diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs index 60f97bdd53..0a8143b0b6 100644 --- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs @@ -4,6 +4,8 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} module UnliftedNewtypesUnassociatedFamily where @@ -20,7 +22,16 @@ newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep]) data instance DFT 'LiftedRep = MkDFT4 | MkDFT5 data family DF :: TYPE (r :: RuntimeRep) -newtype instance DF = MkDF1 Int# -newtype instance DF = MkDF2 Word# -newtype instance DF = MkDF3 (# Int#, Word# #) + +-- Use a type application +newtype instance DF @IntRep = MkDF1 Int# + +-- Use a kind signature +newtype instance DF :: TYPE 'WordRep where + MkDF2 :: Word# -> DF + +-- Also uses a kind signature +newtype instance DF :: TYPE ('TupleRep '[ 'IntRep, 'WordRep ]) where + MkDF3 :: (# Int#, Word# #) -> DF + data instance DF = MkDF4 | MkDF5 diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs index 3984df496a..44a458b5eb 100644 --- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs @@ -10,14 +10,14 @@ module UnliftedNewtypesUnassociatedFamily where import GHC.Int (Int(I#)) -import GHC.Exts (Int#,Word#,RuntimeRep(IntRep)) +import GHC.Exts (Int#,Word#,RuntimeRep(IntRep,WordRep)) import GHC.Exts (TYPE) type KindOf (a :: TYPE k) = k data family D (a :: TYPE r) :: TYPE r -newtype instance D a = MkWordD Word# +newtype instance D (a :: TYPE 'WordRep) = MkWordD Word# -newtype instance D a :: TYPE (KindOf a) where - MkIntD :: forall a. Int# -> D a +newtype instance D (a :: TYPE 'IntRep) :: TYPE (KindOf a) where + MkIntD :: forall (b :: TYPE 'IntRep). Int# -> D b diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 5aeb4d0a58..3a36e77922 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -736,3 +736,4 @@ test('InstanceGivenOverlap', normal, compile, ['']) test('InstanceGivenOverlap2', normal, compile, ['']) test('LocalGivenEqs', normal, compile, ['']) test('LocalGivenEqs2', normal, compile, ['']) +test('T18891', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T18891a.hs b/testsuite/tests/typecheck/should_fail/T18891a.hs new file mode 100644 index 0000000000..d211fc94f2 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18891a.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs, UnliftedNewtypes, StandaloneKindSignatures, RankNTypes, TypeFamilies, PolyKinds #-} + +module T18891 where + +import GHC.Exts( TYPE ) + +newtype N1 :: forall k. TYPE k where + MkN1 :: N1 -> N1 + +type N2 :: forall k. TYPE k +newtype N2 :: forall k. TYPE k where + MkN2 :: N2 -> N2 + diff --git a/testsuite/tests/typecheck/should_fail/T18891a.stderr b/testsuite/tests/typecheck/should_fail/T18891a.stderr new file mode 100644 index 0000000000..881924c8a1 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18891a.stderr @@ -0,0 +1,12 @@ + +T18891a.hs:8:4: error: + • A newtype constructor must have a return type of form T a1 ... an + MkN1 :: N1 -> N1 + • In the definition of data constructor ‘MkN1’ + In the newtype declaration for ‘N1’ + +T18891a.hs:12:3: error: + • A newtype constructor must have a return type of form T a1 ... an + MkN2 :: N2 -> N2 + • In the definition of data constructor ‘MkN2’ + In the newtype declaration for ‘N2’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr index 05f3a935eb..d609c850b7 100644 --- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr @@ -1,11 +1,5 @@ -UnliftedNewtypesFamilyKindFail2.hs:12:20: - Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’ - In the first argument of ‘F’, namely ‘5’ - In the newtype instance declaration for ‘F’ - -UnliftedNewtypesFamilyKindFail2.hs:12:31: - Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’ - In the first argument of ‘F’, namely ‘5’ - In the type ‘(F 5)’ - In the definition of data constructor ‘MkF’ +UnliftedNewtypesFamilyKindFail2.hs:12:20: error: + • Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’ + • In the first argument of ‘F’, namely ‘5’ + In the newtype instance declaration for ‘F’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs new file mode 100644 index 0000000000..adac27fe90 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE GADTs #-} + +module UnliftedNewtypesUnassociatedFamily where + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#) +import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep)) + +data family DF :: TYPE (r :: RuntimeRep) + +-- All these fail: see #18891 and !4419 +-- See Note [Kind inference for data family instances] +-- in GHC.Tc.TyCl.Instance +newtype instance DF = MkDF1a Int# +newtype instance DF = MkDF2a Word# +newtype instance DF = MkDF3a (# Int#, Word# #) diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr new file mode 100644 index 0000000000..972f873e62 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr @@ -0,0 +1,18 @@ + +UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error: + • Expecting a lifted type, but ‘Int#’ is unlifted + • In the type ‘Int#’ + In the definition of data constructor ‘MkDF1a’ + In the newtype instance declaration for ‘DF’ + +UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error: + • Expecting a lifted type, but ‘Word#’ is unlifted + • In the type ‘Word#’ + In the definition of data constructor ‘MkDF2a’ + In the newtype instance declaration for ‘DF’ + +UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error: + • Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted + • In the type ‘(# Int#, Word# #)’ + In the definition of data constructor ‘MkDF3a’ + In the newtype instance declaration for ‘DF’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 958811d428..913d6d8029 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -546,6 +546,7 @@ test('UnliftedNewtypesConstraintFamily', normal, compile_fail, ['']) test('UnliftedNewtypesMismatchedKind', normal, compile_fail, ['']) test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, ['']) test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, ['']) +test('UnliftedNewtypesUnassociatedFamilyFail', normal, compile_fail, ['']) test('T13834', normal, compile_fail, ['']) test('T17077', normal, compile_fail, ['']) test('T16512a', normal, compile_fail, ['']) @@ -591,3 +592,4 @@ test('T18640c', normal, compile_fail, ['']) test('T10709', normal, compile_fail, ['']) test('T10709b', normal, compile_fail, ['']) test('GivenForallLoop', normal, compile_fail, ['']) +test('T18891a', normal, compile_fail, ['']) |