Do not check synonym RHS for ambiguity
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 29 Feb 2016 14:12:28 +0000 (14:12 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 1 Mar 2016 17:08:32 +0000 (17:08 +0000)
With this patch we no longer check the RHS of a type synonym
declaration for ambiguity.  It only affects type synonyms with foralls
on the RHS (which are rare in the first place), and it's arguably
over-aggressive to check them for ambiguity.  See TcValidity
Note [When we don't check for ambiguity]

This fixes the ASSERT failures in
   th                        T3100
   typecheck/should_compile  T3692
   typecheck/should_fail     T3592

compiler/typecheck/TcValidity.hs

index 784cfa0..99a9be3 100644 (file)
@@ -216,13 +216,10 @@ checkAmbiguity ctxt ty
 
 wantAmbiguityCheck :: UserTypeCtxt -> Bool
 wantAmbiguityCheck ctxt
-  = case ctxt of
-      GhciCtxt -> False  -- Allow ambiguous types in GHCi's :kind command
-                         -- E.g.   type family T a :: *  -- T :: forall k. k -> *
-                         -- Then :k T should work in GHCi, not complain that
-                         -- (T k) is ambiguous!
-      _ -> True
-
+  = case ctxt of  -- See Note [When we don't check for ambiguity]
+      GhciCtxt     -> False
+      TySynCtxt {} -> False
+      _            -> True
 
 checkUserTypeError :: Type -> TcM ()
 -- Check to see if the type signature mentions "TypeError blah"
@@ -247,7 +244,26 @@ checkUserTypeError = check
                      ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
 
 
-{-
+{- Note [When we don't check for ambiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a few places we do not want to check a user-specified type for ambiguity
+
+* GhciCtxt: Allow ambiguous types in GHCi's :kind command
+  E.g.   type family T a :: *  -- T :: forall k. k -> *
+  Then :k T should work in GHCi, not complain that
+  (T k) is ambiguous!
+
+* TySynCtxt: type T a b = C a b => blah
+  It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
+  cure the ambiguity.  So we defer the ambiguity check to the use site.
+
+  There is also an implementation reason (Trac #11608).  In the RHS of
+  a type synonym we don't (currently) instantiate 'a' and 'b' with
+  TcTyVars before calling checkValidType, so we get asertion failures
+  from doing an ambiguity check on a type with TyVars in it.  Fixing this
+  would not be hard, but let's wait till there's a reason.
+
+
 ************************************************************************
 *                                                                      *
           Checking validity of a user-defined type
@@ -472,13 +488,12 @@ check_type env ctxt rank ty
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
     tau_kind          = typeKind tau
+    (env', _)         = tidyTyCoVarBndrs env tvs
 
     phi_kind | null theta = tau_kind
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
 
-    (env', _)         = tidyTyCoVarBndrs env tvs
-
 check_type _ _ _ (TyVarTy _) = return ()
 
 check_type env ctxt rank (ForAllTy (Anon arg_ty) res_ty)