Make isInsolubleOccursCheck more aggressive
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 May 2017 08:27:08 +0000 (09:27 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 May 2017 08:32:29 +0000 (09:32 +0100)
Consider
  type family F a :: * -> *

Then (a ~ F Int a) is an insoluble occurs check, and can be reported
as such.  Previous to this patch, TcType.isInsolubleOccursCheck was
treating any type-family application (including an over-saturated one)
as unconditionally not-insoluble.

This really only affects error messages, and then only slightly. I
tripped over this when investigating  Trac #13674.

compiler/typecheck/TcType.hs

index ab2f843..bd72981 100644 (file)
@@ -2152,7 +2152,9 @@ isInsolubleOccursCheck eq_rel tv ty
     go (CoercionTy _) = False   -- ToDo: what about the coercion
     go (TyConApp tc tys)
       | isGenerativeTyCon tc role = any go tys
-      | otherwise                 = False
+      | otherwise                 = any go (drop (tyConArity tc) tys)
+         -- (a ~ F b a), where F has arity 1,
+         -- has an insoluble occurs check
 
     role = eqRelRole eq_rel