Check for equality before deferring
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 4 Mar 2015 13:18:57 +0000 (13:18 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 4 Mar 2015 13:19:35 +0000 (13:19 +0000)
This one was a bit of a surprise. In fixing Trac #7854, I moved
the checkAmbiguity tests to checkValidType. That meant it happened
even for monotypes, and that turned out to be very expensive in
T9872a, for reasons described in this (new) Note in TcUnify:

    Note [Check for equality before deferring]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Particularly in ambiguity checks we can get equalities like (ty ~ ty).
    If ty involves a type function we may defer, which isn't very sensible.
    An egregious example of this was in test T9872a, which has a type signature
           Proxy :: Proxy (Solutions Cubes)
    Doing the ambiguity check on this signature generates the equality
       Solutions Cubes ~ Solutions Cubes
    and currently the constraint solver normalises both sides at vast cost.
    This little short-cut in 'defer' helps quite a bit.

I fixed the problem with a quick equality test, but it feels like an ad-hoc
solution; I think we might want to do something in the constraint solver too.

(The problem was there all along, just more hidden.)

compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs

index 32a04de..f732515 100644 (file)
@@ -738,14 +738,15 @@ uType origin orig_ty1 orig_ty2
         -- Always defer if a type synonym family (type function)
         -- is involved.  (Data families behave rigidly.)
     go ty1@(TyConApp tc1 _) ty2
-      | isTypeFamilyTyCon tc1 = uType_defer origin ty1 ty2
+      | isTypeFamilyTyCon tc1 = defer ty1 ty2
     go ty1 ty2@(TyConApp tc2 _)
-      | isTypeFamilyTyCon tc2 = uType_defer origin ty1 ty2
+      | isTypeFamilyTyCon tc2 = defer ty1 ty2
 
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
       | tc1 == tc2, length tys1 == length tys2
-      = do { cos <- zipWithM (uType origin) tys1 tys2
+      = ASSERT( isDecomposableTyCon tc1 )
+        do { cos <- zipWithM (uType origin) tys1 tys2
            ; return $ mkTcTyConAppCo Nominal tc1 cos }
 
     go (LitTy m) ty@(LitTy n)
@@ -770,7 +771,12 @@ uType origin orig_ty1 orig_ty2
 
         -- Anything else fails
         -- E.g. unifying for-all types, which is relative unusual
-    go ty1 ty2 = uType_defer origin ty1 ty2 -- failWithMisMatch origin
+    go ty1 ty2 = defer ty1 ty2
+
+    ------------------
+    defer ty1 ty2   -- See Note [Check for equality before deferring]
+      | ty1 `tcEqType` ty2 = return (mkTcNomReflCo ty1)
+      | otherwise          = uType_defer origin ty1 ty2
 
     ------------------
     go_app s1 t1 s2 t2
@@ -778,7 +784,17 @@ uType origin orig_ty1 orig_ty2
            ; co_t <- uType origin t1 t2
            ; return $ mkTcAppCo co_s co_t }
 
-{-
+{- Note [Check for equality before deferring]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Particularly in ambiguity checks we can get equalities like (ty ~ ty).
+If ty involves a type function we may defer, which isn't very sensible.
+An egregious example of this was in test T9872a, which has a type signature
+       Proxy :: Proxy (Solutions Cubes)
+Doing the ambiguity check on this signature generates the equality
+   Solutions Cubes ~ Solutions Cubes
+and currently the constraint solver normalises both sides at vast cost.
+This little short-cut in 'defer' helps quite a bit.
+
 Note [Care with type applications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Note: type applications need a bit of care!
index 3988af4..3d01f50 100644 (file)
@@ -296,6 +296,8 @@ checkValidType ctxt ty
        ; check_kind ctxt ty
 
        -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
+       -- NB: this will happen even for monotypes, but that should be cheap;
+       --     and there may be nested foralls for the subtype test to examine
        ; checkAmbiguity ctxt ty
 
        ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }