Propagate ReturnTvs in matchExpectedFunTys
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 11 Feb 2015 18:40:21 +0000 (13:40 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 11 Feb 2015 20:30:31 +0000 (15:30 -0500)
This really should have done a while ago, with the ReturnTv factoring.
It's surprising that I can't tickle the bug!

Please merge to ghc-7.10.

compiler/typecheck/TcMType.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/gadt/gadt7.stderr

index 71fc8ff..eb30227 100644 (file)
@@ -19,7 +19,7 @@ module TcMType (
   newFlexiTyVar,
   newFlexiTyVarTy,              -- Kind -> TcM TcType
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
-  newReturnTyVar,
+  newReturnTyVar, newReturnTyVarTy,
   newMetaKindVar, newMetaKindVars,
   mkTcTyVarName, cloneMetaTyVar,
 
@@ -434,6 +434,9 @@ newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 newReturnTyVar :: Kind -> TcM TcTyVar
 newReturnTyVar kind = newMetaTyVar ReturnTv kind
 
+newReturnTyVarTy :: Kind -> TcM TcType
+newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
+
 tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind and type
index 3212065..d6fadc7 100644 (file)
@@ -34,7 +34,7 @@ module TcType (
   MetaDetails(Flexi, Indirect), MetaInfo(..),
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
   isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
-  isFskTyVar, isFmvTyVar, isFlattenTyVar,
+  isFskTyVar, isFmvTyVar, isFlattenTyVar, isReturnTyVar,
   isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   isTypeVar, isKindVar,
@@ -686,7 +686,7 @@ isImmutableTyVar tv
 
 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
   isMetaTyVar, isAmbiguousTyVar,
-  isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool
+  isFmvTyVar, isFskTyVar, isFlattenTyVar, isReturnTyVar :: TcTyVar -> Bool
 
 isTyConableTyVar tv
         -- True of a meta-type variable that can be filled in
@@ -736,6 +736,12 @@ isMetaTyVar tv
         MetaTv {} -> True
         _         -> False
 
+isReturnTyVar tv
+  = ASSERT2( isTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+      MetaTv { mtv_info = ReturnTv } -> True
+      _                              -> False
+
 -- isAmbiguousTyVar is used only when reporting type errors
 -- It picks out variables that are unbound, namely meta
 -- type variables and the RuntimUnk variables created by
index 024d443..689e6f4 100644 (file)
@@ -141,7 +141,7 @@ matchExpectedFunTys herald arity orig_ty
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty' -> go n_req ty'
-               Flexi        -> defer n_req ty }
+               Flexi        -> defer n_req ty (isReturnTyVar tv) }
 
        -- In all other cases we bale out into ordinary unification
        -- However unlike the meta-tyvar case, we are sure that the
@@ -159,15 +159,21 @@ matchExpectedFunTys herald arity orig_ty
        -- But in that case we add specialized type into error context
        -- anyway, because it may be useful. See also Trac #9605.
     go n_req ty = addErrCtxtM mk_ctxt $
-                  defer n_req ty
+                  defer n_req ty False
 
     ------------
-    defer n_req fun_ty
-      = do { arg_tys <- newFlexiTyVarTys n_req openTypeKind
+    -- If we decide that a ReturnTv (see Note [ReturnTv] in TcType) should
+    -- really be a function type, then we need to allow the argument and
+    -- result types also to be ReturnTvs.
+    defer n_req fun_ty is_return
+      = do { arg_tys <- mapM new_ty_var_ty (nOfThem n_req openTypeKind)
                         -- See Note [Foralls to left of arrow]
-           ; res_ty  <- newFlexiTyVarTy openTypeKind
+           ; res_ty  <- new_ty_var_ty openTypeKind
            ; co   <- unifyType fun_ty (mkFunTys arg_tys res_ty)
            ; return (co, arg_tys, res_ty) }
+      where
+        new_ty_var_ty | is_return = newReturnTyVarTy
+                      | otherwise = newFlexiTyVarTy
 
     ------------
     mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
@@ -992,7 +998,7 @@ checkTauTvUpdate dflags tv ty
   where
     details = ASSERT2( isMetaTyVar tv, ppr tv ) tcTyVarDetails tv
     info         = mtv_info details
-    is_return_tv = case info of { ReturnTv -> True; _ -> False }
+    is_return_tv = isReturnTyVar tv
     impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
 
     defer_me :: TcType -> Bool
index 603cf5b..89c05c5 100644 (file)
@@ -1,19 +1,19 @@
 
 gadt7.hs:16:38:
-    Couldn't match expected type ‘t’ with actual type ‘t1
-      ‘t1’ is untouchable
-        inside the constraints: t2 ~ Int
+    Couldn't match expected type ‘t’ with actual type ‘r
+      ‘r’ is untouchable
+        inside the constraints: t1 ~ Int
         bound by a pattern with constructor: K :: T Int,
                  in a case alternative
         at gadt7.hs:16:33
-      ‘t1’ is a rigid type variable bound by
-           the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
+      ‘r’ is a rigid type variable bound by
+          the inferred type of i1b :: T t1 -> r -> t at gadt7.hs:16:1
       ‘t’ is a rigid type variable bound by
-          the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
+          the inferred type of i1b :: T t1 -> r -> t at gadt7.hs:16:1
     Possible fix: add a type signature for ‘i1b’
     Relevant bindings include
-      y1 :: t1 (bound at gadt7.hs:16:16)
-      y :: t1 (bound at gadt7.hs:16:7)
-      i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)
+      y1 :: r (bound at gadt7.hs:16:16)
+      y :: r (bound at gadt7.hs:16:7)
+      i1b :: T t1 -> r -> t (bound at gadt7.hs:16:1)
     In the expression: y1
     In a case alternative: K -> y1