Rejig the error messages a bit; fixes a minor bug

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

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index bfe5207..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.

@@ -113,37 +117,41 @@ data Rewrite = Rewrite TcType           -- lhs of rewrite rule
                        TcType           -- rhs of rewrite rule
                        TcType           -- coercion witnessing the rewrite rule
 
                        TcType           -- rhs of rewrite rule
                        TcType           -- coercion witnessing the rewrite rule
 

-eqInstToRewrite :: Inst -> Maybe Rewrite
+eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
+                                           -- True iff rewrite swapped equality

 eqInstToRewrite inst
   = ASSERT( isEqInst inst )
 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
 

-    -- rewrite type family applications
+    -- left-to-right rule with type family head

     go ty1@(TyConApp con _) ty2 co 
       | isOpenSynTyCon con
     go ty1@(TyConApp con _) ty2 co 
       | isOpenSynTyCon con

-      = Just $ Rewrite ty1 ty2 co
+      = Just (Rewrite ty1 ty2 co, False)                     -- not swapped

 
 

-    -- rewrite skolems
+    -- left-to-right rule with type variable head

     go ty1@(TyVarTy tv) ty2 co 
       | isSkolemTyVar tv
     go ty1@(TyVarTy tv) ty2 co 
       | isSkolemTyVar tv

-      = Just $ Rewrite ty1 ty2 co
+      = Just (Rewrite ty1 ty2 co, False)                     -- not swapped

 
 

-    -- rewrite type family applications from right-to-left, only after
+    -- right-to-left rule with type family head, only after

     -- having checked whether we can work left-to-right
     go ty1 ty2@(TyConApp con _) co 
       | isOpenSynTyCon con
     -- having checked whether we can work left-to-right
     go ty1 ty2@(TyConApp con _) co 
       | isOpenSynTyCon con

-      = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
+      = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped

 
 

-    -- rewrite skolems from right-to-left, only after having checked
-    -- whether we can work left-to-right 
+    -- right-to-left rule with type variable head, only after 
+    -- having checked whether we can work left-to-right 

     go ty1 ty2@(TyVarTy tv) co 
       | isSkolemTyVar tv
     go ty1 ty2@(TyVarTy tv) co 
       | isSkolemTyVar tv

-      = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
+      = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped

 
 

+    -- this equality is not a rewrite rule => ignore

     go _ _ _ = Nothing
 \end{code}
 
     go _ _ _ = Nothing
 \end{code}
 

@@ -156,8 +164,8 @@ explicitly given elementary rewrite.
 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
 tcEqInstNormaliseFamInst inst ty
   = case eqInstToRewrite inst of
 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
 tcEqInstNormaliseFamInst inst ty
   = case eqInstToRewrite inst of

-      Just rewrite -> tcEqRuleNormaliseFamInst rewrite ty
-      Nothing      -> return (IdCo, ty)
+      Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
+      Nothing           -> return (IdCo, ty)

 
 -- Rewrite by equality rewrite rule
 tcEqRuleNormaliseFamInst :: Rewrite                     -- elementary rewrite
 
 -- Rewrite by equality rewrite rule
 tcEqRuleNormaliseFamInst :: Rewrite                     -- elementary rewrite

@@ -489,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 

@@ -534,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

@@ -543,38 +590,21 @@ skolemOccurs insts
   where
     oneSkolemOccurs inst
       = ASSERT( isEqInst inst )
   where
     oneSkolemOccurs inst
       = ASSERT( isEqInst inst )

-        isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
+        case eqInstToRewrite inst of
+          Just (rewrite, swapped) -> breakRecursion rewrite swapped
+          Nothing                 -> return ([inst], return ())

       where
       where

+        -- inst is an elementary rewrite rule, check whether we need to break
+        -- it up
+        breakRecursion (Rewrite pat body _) swapped

 
 

-        -- look through synonyms
-        isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
-        isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
-
-        -- left-to-right rule with type family head
-        isRewriteRule ty1@(TyConApp con _) ty2
-          | isOpenSynTyCon con
-          = breakRecursion ty1 ty2 False    -- not swapped
-
-        -- left-to-right rule with type variable head
-        isRewriteRule ty1@(TyVarTy _) ty2
-          = breakRecursion ty1 ty2 False    -- not swapped
-
-        -- right-to-left rule with type family head
-        isRewriteRule ty1 ty2@(TyConApp con _)
-          | isOpenSynTyCon con
-          = breakRecursion ty2 ty1 True     -- swapped
-
-        -- right-to-left rule with type variable head
-        isRewriteRule ty1 ty2@(TyVarTy _)
-          = breakRecursion ty2 ty1 True     -- swapped
-
-        -- this equality is not a rewrite rule => ignore
-        isRewriteRule _ _ = return ([inst], return ())
-
-        ------------------
-        breakRecursion pat body swapped
+          -- skolemOccurs does not apply, leave as is

           | null tysToLiftOut 
           | 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
           = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
                ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
           | otherwise
           = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
                ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut

@@ -642,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}
 
 

@@ -674,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' 

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

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

 \end{code}
 
 
 \end{code}
 
 

@@ -848,8 +877,8 @@ substRule insts = tryAllInsts insts []
 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 substInst inst insts
   = case eqInstToRewrite inst of
 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 substInst inst insts
   = case eqInstToRewrite inst of

-      Just rewrite -> substEquality rewrite insts
-      Nothing      -> return (insts, False)
+      Just (rewrite, _) -> substEquality rewrite insts
+      Nothing           -> return (insts, False)

   where
     substEquality :: Rewrite            -- elementary rewrite
                   -> [Inst]             -- insts to rewrite
   where
     substEquality :: Rewrite            -- elementary rewrite
                   -> [Inst]             -- insts to rewrite

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

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

 \end{code}
 
 
 \end{code}
 
 

@@ -931,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

@@ -1173,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}