Fix #15859 by checking, not assuming, an ArgFlag
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 5 Nov 2018 16:01:47 +0000 (11:01 -0500)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 5 Nov 2018 18:52:31 +0000 (13:52 -0500)
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

compiler/typecheck/TcExpr.hs
testsuite/tests/dependent/should_fail/T15859.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T

index f27922f..a087917 100644 (file)
@@ -1329,14 +1329,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.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr
new file mode 100644 (file)
index 0000000..e479404
--- /dev/null
@@ -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
index d76fc35..f127220 100644 (file)
@@ -38,3 +38,4 @@ test('T15591c', normal, compile_fail, [''])
 test('T15743c', normal, compile_fail, [''])
 test('T15743d', normal, compile_fail, [''])
 test('T15825', normal, compile_fail, [''])
+test('T15859', normal, compile_fail, [''])