X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=4e3f72835bc474af0595a75bf296434d5b56a9da;hb=eb731f1519b868fa9686f2a56280dd1aaf8edc9d;hp=f7c21afd13af5bed82a15a882842bade93b5d930;hpb=41184261859b64fa03c026d39f627f7f4dab94eb;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index f7c21af..4e3f728 100644
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -103,7 +103,11 @@ An elementary rewrite is a properly oriented equality with associated coercion
 that has one of the following two forms:
 
 (1) co :: F t1..tn ~ t
-(2) co :: a ~ t         , where t /= F t1..tn
+(2) co :: a ~ t         , where t /= F t1..tn and a is a skolem tyvar
+
+NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
+reqrite rule.  Instead, such equalities are solved by unification.  This is
+essential; cf Note [skolemOccurs loop].
 
 The following functions takes an equality instance and turns it into an
 elementary rewrite if possible.
@@ -491,7 +495,7 @@ oriented properly, like
 
      F a ~ [G (F a)]
  or even
-     a ~ [G a]
+     a ~ [G a]          , where a is a skolem tyvar
 
 The left-to-right orientiation is not suitable because it does not
 terminate. The right-to-left orientation is not suitable because it 
@@ -536,6 +540,45 @@ NB: We perform this transformation for multiple occurences of ty1 under one
     rule doesn't need to be applied multiple times at a single inst).  As a 
     result we can get two or more insts back.
 
+Note [skolemOccurs loop]
+~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that under
+
+  type family F a 
+  type instance F [a] = [F a]
+
+a signature such as
+
+  foo :: (F [a] ~ a) => a
+
+will get us into a loop.  However, this is *not* the case.  Here is why:
+
+    F [a<sk>] ~ a<sk>
+
+    -->(TOP)
+
+    [F a<sk>] ~ a<sk>
+
+    -->(SkolemOccurs)
+
+    [b<tau>] ~ a<sk>
+    F [b<tau>] ~ b<tau>   , with b := F a
+
+    -->(TOP)
+
+    [b<tau>] ~ a<sk>
+    [F b<tau>] ~ b<tau>   , with b := F a
+
+At this point (SkolemOccurs) does *not* apply anymore, as 
+
+  [F b<tau>] ~ b<tau>
+
+is not used as a rewrite rule.  The variable b<tau> is not a skolem (cf
+eqInstToRewrite). 
+
+(The regression test indexed-types/should_compile/Simple20 checks that the
+described property of the system does not change.)
+
 \begin{code}
 skolemOccurs :: PrecondRule
 skolemOccurs insts
@@ -555,7 +598,9 @@ skolemOccurs insts
 
           -- skolemOccurs does not apply, leave as is
           | null tysToLiftOut 
-          = return ([inst], return ())
+          = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
+               ; return ([inst], return ())
+               }
 
           -- recursive occurence of pat in body under a type family application
           | otherwise
@@ -1191,7 +1236,7 @@ ppr_ty env ty
 -- (ppr_extra env ty) shows extra info about 'ty'
 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
 ppr_extra env (TyVarTy tv)
-  | isSkolemTyVar tv || isSigTyVar tv
+  | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv)
   = return (env1, pprSkolTvBinding tv1)
   where
     (env1, tv1) = tidySkolemTyVar env tv