Reorganise TcSimplify (again); FIX Trac #1919

[ghc-hetmet.git] / compiler / typecheck / TcTyFuns.lhs

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index f7c21af..d7da2f7 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -11,7 +11,7 @@ module TcTyFuns (
        substEqInDictInsts,
        
         -- errors
        substEqInDictInsts,
        
         -- errors

-        eqInstMisMatch, misMatchMsg,
+        misMatchMsg, failWithMisMatch

   ) where
 
 
   ) where
 
 

@@ -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
 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.
 
 The following functions takes an equality instance and turns it into an
 elementary rewrite if possible.

@@ -117,8 +121,10 @@ eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
                                            -- True iff rewrite swapped equality
 eqInstToRewrite inst
   = ASSERT( isEqInst inst )
                                            -- True iff rewrite swapped equality
 eqInstToRewrite inst
   = ASSERT( isEqInst inst )

-    go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
+    go ty1 ty2 (eqInstType inst)

   where
   where

+    (ty1,ty2) = eqInstTys inst
+

     -- look through synonyms
     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
     -- look through synonyms
     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co

@@ -491,7 +497,7 @@ oriented properly, like
 
      F a ~ [G (F a)]
  or even
 
      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 
 
 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 +542,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.
 
     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
 \begin{code}
 skolemOccurs :: PrecondRule
 skolemOccurs insts

@@ -555,7 +600,9 @@ skolemOccurs insts
 
           -- skolemOccurs does not apply, leave as is
           | null tysToLiftOut 
 
           -- 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
 
           -- recursive occurence of pat in body under a type family application
           | otherwise

@@ -625,8 +672,7 @@ trivialRule insts
       | otherwise
       = return $ Just inst
       where
       | otherwise
       = return $ Just inst
       where

-        ty1 = eqInstLeftTy  inst
-        ty2 = eqInstRightTy inst
+        (ty1,ty2) = eqInstTys inst

 \end{code}
 
 
 \end{code}
 
 

@@ -657,8 +703,9 @@ decompRule insts
   where
     decomp inst
       = ASSERT( isEqInst inst )
   where
     decomp inst
       = ASSERT( isEqInst inst )

-        go (eqInstLeftTy inst) (eqInstRightTy inst)
+        go ty1 ty2

       where
       where

+       (ty1,ty2) = eqInstTys inst

         go ty1 ty2             
           | Just ty1' <- tcView ty1 = go ty1' ty2 
           | Just ty2' <- tcView ty2 = go ty1 ty2' 
         go ty1 ty2             
           | Just ty1' <- tcView ty1 = go ty1' ty2 
           | Just ty2' <- tcView ty2 = go ty1 ty2' 

@@ -777,8 +824,7 @@ topRule insts
                    }
             }
       where
                    }
             }
       where

-        ty1 = eqInstLeftTy  inst
-       ty2 = eqInstRightTy inst
+        (ty1,ty2) = eqInstTys inst

 \end{code}
 
 
 \end{code}
 
 

@@ -876,8 +922,7 @@ substInst inst insts
                     }
               }
          where 
                     }
               }
          where 

-            ty1 = eqInstLeftTy  inst
-            ty2 = eqInstRightTy inst
+            (ty1,ty2) = eqInstTys inst

 \end{code}
 
 
 \end{code}
 
 

@@ -914,9 +959,10 @@ unifyMetaRule insts
   where
     unifyMeta inst
       = ASSERT( isEqInst inst )
   where
     unifyMeta inst
       = ASSERT( isEqInst inst )

-        go (eqInstLeftTy inst) (eqInstRightTy inst)
+        go ty1 ty2

            (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
       where
            (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
       where

+       (ty1,ty2) = eqInstTys inst

         go ty1 ty2 cotv
           | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
           | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
         go ty1 ty2 cotv
           | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
           | Just ty2' <- tcView ty2 = go ty1 ty2' cotv

@@ -1156,45 +1202,49 @@ somethingdifferent message.
 eqInstMisMatch :: Inst -> TcM a
 eqInstMisMatch inst
   = ASSERT( isEqInst inst )
 eqInstMisMatch :: Inst -> TcM a
 eqInstMisMatch inst
   = ASSERT( isEqInst inst )

-    do { (env, msg) <- misMatchMsg ty_act ty_exp
-       ; setErrCtxt ctxt $
-           failWithTcM (env, msg)
-       }
+    setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp

   where
   where

-    ty_act           = eqInstLeftTy  inst
-    ty_exp           = eqInstRightTy inst
-    InstLoc _ _ ctxt = instLoc       inst
+    (ty_act, ty_exp) = eqInstTys inst
+    InstLoc _ _ ctxt = instLoc   inst

 
 -----------------------
 
 -----------------------

-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
+failWithMisMatch :: TcType -> TcType -> TcM a

 -- Generate the message when two types fail to match,
 -- going to some trouble to make it helpful.
 -- The argument order is: actual type, expected type
 -- Generate the message when two types fail to match,
 -- going to some trouble to make it helpful.
 -- The argument order is: actual type, expected type

-misMatchMsg ty_act ty_exp
+failWithMisMatch ty_act ty_exp

   = do { env0 <- tcInitTidyEnv
         ; ty_exp <- zonkTcType ty_exp
         ; ty_act <- zonkTcType ty_act
   = do { env0 <- tcInitTidyEnv
         ; ty_exp <- zonkTcType ty_exp
         ; ty_act <- zonkTcType ty_act

-       ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
-       ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
-       ; return (env2, 
-                  sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
-                           nest 7 $
+        ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
+       }
+
+misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
+misMatchMsg env0 (ty_act, ty_exp)
+  = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
+       (env2, pp_act, extra_act) = ppr_ty env1 ty_act
+        msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
+                       nest 7 $

                               ptext SLIT("against inferred type") <+> pp_act],
                               ptext SLIT("against inferred type") <+> pp_act],

-                      nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do { let (env1, tidy_ty) = tidyOpenType env ty
-       ; (env2, extra) <- ppr_extra env1 tidy_ty
-       ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (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
-  = return (env1, pprSkolTvBinding tv1)
+                  nest 2 (extra_exp $$ extra_act)]
+    in
+    (env2, msg)
+

   where
   where

-    (env1, tv1) = tidySkolemTyVar env tv
+    ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
+    ppr_ty env ty
+      = let (env1, tidy_ty) = tidyOpenType env ty
+           (env2, extra)  = ppr_extra env1 tidy_ty
+       in
+       (env2, quotes (ppr tidy_ty), extra)
+
+    -- (ppr_extra env ty) shows extra info about 'ty'
+    ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
+    ppr_extra env (TyVarTy tv)
+      | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
+      = (env1, pprSkolTvBinding tv1)
+      where
+        (env1, tv1) = tidySkolemTyVar env tv

 
 

-ppr_extra env _ty = return (env, empty)                -- Normal case
+    ppr_extra env _ty = (env, empty)           -- Normal case

 \end{code}
 \end{code}