diff options
| author | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-11-05 11:01:47 -0500 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2018-11-22 17:04:06 -0500 |
| commit | 2594ea25641e4b27327449d40c5dd2d46d837af1 (patch) | |
| tree | f2d394c6d00ec1972278ba4c0ea380a619854c37 | |
| parent | 64a5044543bdcd7983787b215a44bdfb70c9c40b (diff) | |
| download | haskell-2594ea25641e4b27327449d40c5dd2d46d837af1.tar.gz | |
Fix #15859 by checking, not assuming, an ArgFlag
We thought that visible dependent quantification was impossible
in terms, but Iceland Jack discovered otherwise in #15859. This fixes an
ASSERT failure that arose.
test case: dependent/should_fail/T15859
(cherry picked from commit 72b82343b79365dc74ffafb345dd33499a7fd394)
(cherry picked from commit 5693ddd071033516a1804420a903cb7e3677682b)
| -rw-r--r-- | compiler/typecheck/TcExpr.hs | 10 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T15859.hs | 13 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T15859.stderr | 6 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/all.T | 1 |
4 files changed, 24 insertions, 6 deletions
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 4751a20446..8557af2f72 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -1330,14 +1330,12 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty -- wrap1 :: fun_ty "->" upsilon_ty ; case tcSplitForAllTy_maybe upsilon_ty of - Just (tvb, inner_ty) -> + Just (tvb, inner_ty) + | binderArgFlag tvb == Specified -> + -- It really can't be Inferred, because we've just instantiated those + -- But, oddly, it might just be Required. See #15859. do { let tv = binderVar tvb - vis = binderArgFlag tvb kind = tyVarKind tv - ; MASSERT2( vis == Specified - , (vcat [ ppr fun_ty, ppr upsilon_ty, ppr tvb - , ppr inner_ty, pprTyVar tv - , ppr vis ]) ) ; ty_arg <- tcHsTypeApp hs_ty_arg kind ; inner_ty <- zonkTcType inner_ty diff --git a/testsuite/tests/dependent/should_fail/T15859.hs b/testsuite/tests/dependent/should_fail/T15859.hs new file mode 100644 index 0000000000..e8ffdf4ae2 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15859.hs @@ -0,0 +1,13 @@ +{-# Language PolyKinds #-} +{-# Language TypeApplications #-} +{-# Language ImpredicativeTypes #-} + +module T15859 where + +import Data.Kind + +data A k :: k -> Type + +type KindOf (a :: k) = k + +a = (undefined :: KindOf A) @Int diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr new file mode 100644 index 0000000000..e4794048b7 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15859.stderr @@ -0,0 +1,6 @@ + +T15859.hs:13:5: error: + • Cannot apply expression of type ‘forall k -> k -> *’ + to a visible type argument ‘Int’ + • In the expression: (undefined :: KindOf A) @Int + In an equation for ‘a’: a = (undefined :: KindOf A) @Int diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 593b7787a1..d006175904 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -35,3 +35,4 @@ test('T15215', normal, compile_fail, ['']) test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds']) test('T15343', normal, compile_fail, ['']) test('T15380', normal, compile_fail, ['']) +test('T15859', normal, compile_fail, ['']) |