Commit 2c133b67 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Really fix Trac #14158

I dug more into how #14158 started working. I temporarily reverted the
patch that "fixed" it, namely

    commit a6c448b4
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Mon Aug 28 17:33:59 2017 +0100

    Small refactor of getRuntimeRep

Sure enough, there was a real bug, described in the new
TcExpr Note [Visible type application zonk]

In general, syntactic substituion should be kind-preserving!
Maybe we should check that invariant...
parent 3790ea90
...@@ -65,7 +65,7 @@ import PrelNames ...@@ -65,7 +65,7 @@ import PrelNames
import DynFlags import DynFlags
import SrcLoc import SrcLoc
import Util import Util
import VarEnv ( emptyTidyEnv ) import VarEnv ( emptyTidyEnv, mkInScopeSet )
import ListSetOps import ListSetOps
import Maybes import Maybes
import Outputable import Outputable
...@@ -1294,7 +1294,18 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald ...@@ -1294,7 +1294,18 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
, ppr inner_ty, pprTyVar tv , ppr inner_ty, pprTyVar tv
, ppr vis ]) ) , ppr vis ]) )
; ty_arg <- tcHsTypeApp hs_ty_arg kind ; ty_arg <- tcHsTypeApp hs_ty_arg kind
; let insted_ty = substTyWithUnchecked [tv] [ty_arg] inner_ty
; inner_ty <- zonkTcType inner_ty
-- See Note [Visible type application zonk]
; let in_scope = mkInScopeSet (tyCoVarsOfTypes [upsilon_ty, ty_arg])
insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
-- NB: tv and ty_arg have the same kind, so this
-- substitution is kind-respecting
; traceTc "VTA" (vcat [ppr tv, debugPprType kind
, debugPprType ty_arg
, debugPprType (typeKind ty_arg)
, debugPprType insted_ty ])
; (inner_wrap, args', res_ty) ; (inner_wrap, args', res_ty)
<- go acc_args (n+1) insted_ty args <- go acc_args (n+1) insted_ty args
-- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
...@@ -1326,6 +1337,35 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald ...@@ -1326,6 +1337,35 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
text "Cannot apply expression of type" <+> quotes (ppr ty) $$ text "Cannot apply expression of type" <+> quotes (ppr ty) $$
text "to a visible type argument" <+> quotes (ppr arg) } text "to a visible type argument" <+> quotes (ppr arg) }
{- Note [Visible type application zonk]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
* tcHsTypeApp only guarantees that
- ty_arg is zonked
- kind(zonk(tv)) = kind(ty_arg)
(checkExpectedKind zonks as it goes).
So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
and inner_ty. Otherwise we can build an ill-kinded type. An example was
Trac #14158, where we had:
id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
and we had the visible type application
id @(->)
* We instantiated k := kappa, yielding
forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
Here q1 :: RuntimeRep
* Now we substitute
cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
but we must first zonk the inner_ty to get
forall (a :: TYPE q1). cat a a
so that the result of substitution is well-kinded
Failing to do so led to Trac #14158.
-}
---------------- ----------------
tcArg :: LHsExpr GhcRn -- The function (for error messages) tcArg :: LHsExpr GhcRn -- The function (for error messages)
-> LHsExpr GhcRn -- Actual arguments -> LHsExpr GhcRn -- Actual arguments
......
{-# LANGUAGE TypeApplications #-}
module T14158 where
import qualified Control.Category as Cat
foo = (Cat.id @(->) >>=)
...@@ -574,3 +574,4 @@ test('T13984', normal, compile, ['']) ...@@ -574,3 +574,4 @@ test('T13984', normal, compile, [''])
test('T14128', normal, multimod_compile, ['T14128Main', '-v0']) test('T14128', normal, multimod_compile, ['T14128Main', '-v0'])
test('T14149', normal, compile, ['']) test('T14149', normal, compile, [''])
test('T14154', normal, compile, ['']) test('T14154', normal, compile, [''])
test('T14158', normal, compile, [''])
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