[commit: ghc] ghc-8.6: Fix #15859 by checking, not assuming, an ArgFlag (2594ea2)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.6
Link       : http://ghc.haskell.org/trac/ghc/changeset/2594ea25641e4b27327449d40c5dd2d46d837af1/ghc

>---------------------------------------------------------------

commit 2594ea25641e4b27327449d40c5dd2d46d837af1
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Mon Nov 5 11:01:47 2018 -0500

    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)


>---------------------------------------------------------------

2594ea25641e4b27327449d40c5dd2d46d837af1
 compiler/typecheck/TcExpr.hs                        | 10 ++++------
 testsuite/tests/dependent/should_fail/T15859.hs     | 13 +++++++++++++
 testsuite/tests/dependent/should_fail/T15859.stderr |  6 ++++++
 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 4751a20..8557af2 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 0000000..e8ffdf4
--- /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 0000000..e479404
--- /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 593b778..d006175 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, [''])