Don't barf on error message with non-tc tyvars

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

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index bfe5207..4e3f728 100644 (file)
--- 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
 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,7 +117,8 @@ 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 )
     go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
 eqInstToRewrite inst
   = ASSERT( isEqInst inst )
     go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)

@@ -122,28 +127,29 @@ eqInstToRewrite inst
     go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
     go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
 
     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 +162,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 +495,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 +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.
 
     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 +588,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

@@ -848,8 +876,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

@@ -1208,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)
 -- (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
   = return (env1, pprSkolTvBinding tv1)
   where
     (env1, tv1) = tidySkolemTyVar env tv