[commit: ghc] ghc-8.0: Fix #11473. (6e99d03)

git at git.haskell.org git at git.haskell.org
Wed Mar 23 16:37:32 UTC 2016


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

On branch  : ghc-8.0
Link       : http://ghc.haskell.org/trac/ghc/changeset/6e99d03bf44658c3c65a495fce2f413bf784a145/ghc

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

commit 6e99d03bf44658c3c65a495fce2f413bf784a145
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Tue Mar 15 14:27:22 2016 -0400

    Fix #11473.
    
    I've added a check in the zonker for representation polymorphism.
    I don't like having this be in the zonker, but I don't know where
    else to put it. It can't go in TcValidity, because a clever enough
    user could convince the solver to do bogus representation polymorphism
    even though there's nothing obviously wrong in what they wrote.
    Note that TcValidity doesn't run over *expressions*, which is where
    this problem arises.
    
    In any case, the check is simple and it works.
    
    test case: dependent/should_fail/T11473
    
    (cherry picked from commit aade111248dce0834ed83dc4f18c234967b32024)


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

6e99d03bf44658c3c65a495fce2f413bf784a145
 compiler/typecheck/TcHsSyn.hs                      | 64 +++++++++++++++++++---
 .../{typecheck => dependent}/should_fail/T11473.hs | 13 ++++-
 .../tests/dependent/should_fail/T11473.stderr      |  7 +++
 testsuite/tests/dependent/should_fail/all.T        |  1 +
 4 files changed, 75 insertions(+), 10 deletions(-)

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index d84e527..9094533 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -276,6 +276,7 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids
 zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
 zonkIdBndr env id
   = do ty' <- zonkTcTypeToType env (idType id)
+       ensureNotRepresentationPolymorphic id ty'
        return (setIdType id ty')
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
@@ -456,19 +457,34 @@ zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
                         , abe_mono = zonkIdOcc env mono_id
                         , abe_prags = new_prags })
 
-zonk_bind env (AbsBindsSig { abs_tvs         = tyvars
-                           , abs_ev_vars     = evs
-                           , abs_sig_export  = poly
-                           , abs_sig_prags   = prags
-                           , abs_sig_ev_bind = ev_bind
-                           , abs_sig_bind    = bind })
+zonk_bind env outer_bind@(AbsBindsSig { abs_tvs         = tyvars
+                                      , abs_ev_vars     = evs
+                                      , abs_sig_export  = poly
+                                      , abs_sig_prags   = prags
+                                      , abs_sig_ev_bind = ev_bind
+                                      , abs_sig_bind    = lbind })
+  | L bind_loc bind@(FunBind { fun_id      = L loc local
+                             , fun_matches = ms
+                             , fun_co_fn   = co_fn }) <- lbind
   = ASSERT( all isImmutableTyVar tyvars )
     do { (env0, new_tyvars)  <- zonkTyBndrsX env  tyvars
        ; (env1, new_evs)     <- zonkEvBndrsX env0 evs
        ; (env2, new_ev_bind) <- zonkTcEvBinds env1 ev_bind
-       ; new_val_bind        <- zonk_lbind env2 bind
+           -- Inline zonk_bind (FunBind ...) because we wish to skip
+           -- the check for representation-polymorphic binders. The
+           -- local binder in the FunBind in an AbsBindsSig is never actually
+           -- bound in Core -- indeed, that's the whole point of AbsBindsSig.
+           -- just calling zonk_bind causes #11405.
+       ; new_local           <- updateVarTypeM (zonkTcTypeToType env2) local
+       ; (env3, new_co_fn)   <- zonkCoFn env2 co_fn
+       ; new_ms              <- zonkMatchGroup env3 zonkLExpr ms
+           -- If there is a representation polymorphism problem, it will
+           -- be caught here:
        ; new_poly_id         <- zonkIdBndr env2 poly
        ; new_prags           <- zonkSpecPrags env2 prags
+       ; let new_val_bind = L bind_loc (bind { fun_id      = L loc new_local
+                                             , fun_matches = new_ms
+                                             , fun_co_fn   = new_co_fn })
        ; return (AbsBindsSig { abs_tvs         = new_tyvars
                              , abs_ev_vars     = new_evs
                              , abs_sig_export  = new_poly_id
@@ -476,6 +492,9 @@ zonk_bind env (AbsBindsSig { abs_tvs         = tyvars
                              , abs_sig_ev_bind = new_ev_bind
                              , abs_sig_bind    = new_val_bind  }) }
 
+  | otherwise
+  = pprPanic "zonk_bind" (ppr outer_bind)
+
 zonk_bind env (PatSynBind bind@(PSB { psb_id = L loc id
                                     , psb_args = details
                                     , psb_def = lpat
@@ -1624,3 +1643,34 @@ zonkTypeZapping tv
                 | otherwise          = anyTypeOfKind (tyVarKind tv)
        ; writeMetaTyVar tv ty
        ; return ty }
+
+---------------------------------------
+-- | According to the rules around representation polymorphism
+-- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
+-- can have a representation-polymorphic type. This check ensures
+-- that we respect this rule. It is a bit regrettable that this error
+-- occurs in zonking, after which we should have reported all errors.
+-- But it's hard to see where else to do it, because this can be discovered
+-- only after all solving is done. And, perhaps most importantly, this
+-- isn't really a compositional property of a type system, so it's
+-- not a terrible surprise that the check has to go in an awkward spot.
+ensureNotRepresentationPolymorphic
+  :: TcId  -- the id we're checking (for errors only)
+  -> Type  -- its zonked type
+  -> TcM ()
+ensureNotRepresentationPolymorphic id ty
+  = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
+                   -- forall a. a. See, for example, test ghci/scripts/T9140
+    unless (isEmptyVarSet (tyCoVarsOfType ki)) $
+    addErrAt (nameSrcSpan $ idName id) $
+    vcat [ text "The following variable has an unknown runtime representation:"
+         , text "    Var name:" <+> ppr id
+         , text "    Var type:" <+> ppr tidy_ty
+         , text " Type's kind:" <+> ppr tidy_ki
+         , text "Perhaps add a type or kind signature to fix the representation."
+         ]
+  where
+    ki = typeKind ty
+
+    (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
+    tidy_ki             = tidyType tidy_env ki
diff --git a/testsuite/tests/typecheck/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs
similarity index 67%
copy from testsuite/tests/typecheck/should_fail/T11473.hs
copy to testsuite/tests/dependent/should_fail/T11473.hs
index cb9f791..12d95ca 100644
--- a/testsuite/tests/typecheck/should_fail/T11473.hs
+++ b/testsuite/tests/dependent/should_fail/T11473.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
 
 module T11473 where
+
 import GHC.Exts
 import GHC.Types
 
@@ -14,7 +15,13 @@ class BoxIt (a :: TYPE lev) where
 instance BoxIt Char# where boxed x = C# x
 instance BoxIt Char  where boxed = id
 
--- This should be an error: there is no way we can produce code for both Lifted
--- and Unlifted levities
-hello :: forall (lev :: Levity). forall (a :: TYPE lev). BoxIt a => a -> Boxed a
+hello :: forall (r :: RuntimeRep). forall (a :: TYPE r). BoxIt a => a -> Boxed a
 hello x = boxed x
+{-# NOINLINE hello #-}
+
+main :: IO ()
+main = do
+    print $ boxed 'c'#
+    print $ boxed 'c'
+    print $ hello 'c'
+    print $ hello 'c'#
diff --git a/testsuite/tests/dependent/should_fail/T11473.stderr b/testsuite/tests/dependent/should_fail/T11473.stderr
new file mode 100644
index 0000000..7a7cc32
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T11473.stderr
@@ -0,0 +1,7 @@
+
+T11473.hs:19:7: error:
+    The following variable has an unknown runtime representation:
+        Var name: x
+        Var type: a
+     Type's kind: TYPE r
+    Perhaps add a type or kind signature to fix the representation.
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index fc22a2a..b830121 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -13,3 +13,4 @@ test('T11334', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('KindLevelsB', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
+test('T11473', normal, compile_fail, [''])



More information about the ghc-commits mailing list