Commit 2594ea25 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

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 72b82343)

(cherry picked from commit 5693ddd0)
parent 64a50445
......@@ -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
......
{-# 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
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
......@@ -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, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment