projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Monadify typecheck/TcHsType: use do, return and standard monad functions
[ghc-hetmet.git] / compiler / typecheck / TcTyFuns.lhs
diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index f7c21af..82e397f 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
 
 
@@ -40,7 +40,7 @@ import Maybes
 
 -- standard
 import Data.List
 
 -- standard
 import Data.List
-import Control.Monad (liftM)
+import Control.Monad
 \end{code}
 
 
 \end{code}
 
 
@@ -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
@@ -227,7 +233,7 @@ tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
        }
 tcGenericNormaliseFamInst fun (NoteTy note ty1)
   = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
        }
 tcGenericNormaliseFamInst fun (NoteTy note ty1)
   = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
-       ; return (mkNoteTyCoI note coi, NoteTy note nty1)
+       ; return (coi, NoteTy note nty1)
        }
 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
   | isTcTyVar tv
        }
 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
   | isTcTyVar tv
@@ -382,14 +388,18 @@ normalise_dicts
                        -- Fals <=> they are given
        -> TcM ([Inst],TcDictBinds)
 normalise_dicts given_eqs dicts is_wanted
                        -- Fals <=> they are given
        -> TcM ([Inst],TcDictBinds)
 normalise_dicts given_eqs dicts is_wanted
-  = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+> 
+  = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
+                             | otherwise = "normaliseGivenDicts <-"
+                    in
+                    text name <+> ppr dicts <+> 
                     text "with" <+> ppr given_eqs
        ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
                     text "with" <+> ppr given_eqs
        ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
-       ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
+       ; (dicts1, binds1)  <- substEqInDictInsts is_wanted given_eqs dicts0
        ; let binds01 = binds0 `unionBags` binds1
        ; if isEmptyBag binds1
          then return (dicts1, binds01)
        ; let binds01 = binds0 `unionBags` binds1
        ; if isEmptyBag binds1
          then return (dicts1, binds01)
-         else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
+         else do { (dicts2, binds2) <- 
+                      normalise_dicts given_eqs dicts1 is_wanted
                  ; return (dicts2, binds01 `unionBags` binds2) } }
 \end{code}
 
                  ; return (dicts2, binds01 `unionBags` binds2) } }
 \end{code}
 
@@ -491,7 +501,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 +546,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 +604,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
@@ -612,7 +663,7 @@ The following rules exploits the reflexivity of equality:
 \begin{code}
 trivialRule :: IdemRewriteRule
 trivialRule insts 
 \begin{code}
 trivialRule :: IdemRewriteRule
 trivialRule insts 
-  = liftM catMaybes $ mappM trivial insts
+  = liftM catMaybes $ mapM trivial insts
   where
     trivial inst
       | ASSERT( isEqInst inst )
   where
     trivial inst
       | ASSERT( isEqInst inst )
@@ -625,8 +676,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 +707,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 +828,7 @@ topRule insts
                    }
             }
       where
                    }
             }
       where
-        ty1 = eqInstLeftTy  inst
-       ty2 = eqInstRightTy inst
+        (ty1,ty2) = eqInstTys inst
 \end{code}
 
 
 \end{code}
 
 
@@ -876,8 +926,7 @@ substInst inst insts
                     }
               }
          where 
                     }
               }
          where 
-            ty1 = eqInstLeftTy  inst
-            ty2 = eqInstRightTy inst
+            (ty1,ty2) = eqInstTys inst
 \end{code}
 
 
 \end{code}
 
 
@@ -914,9 +963,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
@@ -1034,10 +1084,11 @@ form
 where F is a type family.
 
 \begin{code}
 where F is a type family.
 
 \begin{code}
-substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
+substEqInDictInsts :: Bool      -- whether the *dictionaries* are wanted/given
+                   -> [Inst]    -- given equalities (used as rewrite rules)
                    -> [Inst]    -- dictinaries to be normalised
                    -> TcM ([Inst], TcDictBinds)
                    -> [Inst]    -- dictinaries to be normalised
                    -> TcM ([Inst], TcDictBinds)
-substEqInDictInsts eqInsts dictInsts 
+substEqInDictInsts isWanted eqInsts dictInsts 
   = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
        ; dictInsts' <- 
            foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
   = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
        ; dictInsts' <- 
            foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
@@ -1051,7 +1102,7 @@ substEqInDictInsts eqInsts dictInsts
                                            tci_right = target})
       | isOpenSynTyConApp pattern || isTyVarTy pattern
       = do { (dictInsts', moreDictBinds) <- 
                                            tci_right = target})
       | isOpenSynTyConApp pattern || isTyVarTy pattern
       = do { (dictInsts', moreDictBinds) <- 
-               genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
+               genericNormaliseInsts isWanted applyThisEq dictInsts
            ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
            }
       where
            ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
            }
       where
@@ -1130,7 +1181,13 @@ genericNormaliseInsts isWanted fun insts
                          rhs       = L (instLocSpan loc) cast_expr
                          binds     = instToDictBind target_dict rhs
                      -- return the new inst
                          rhs       = L (instLocSpan loc) cast_expr
                          binds     = instToDictBind target_dict rhs
                      -- return the new inst
-                   ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
+                   ; traceTc $ let name | isWanted 
+                                         = "genericNormaliseInst (wanted) ->"
+                                         | otherwise
+                                         = "genericNormaliseInst (given) ->"
+                                in
+                                text name <+> ppr dict' <+>
+                                text "with" <+> ppr binds
                     ; return (dict', binds)
                    }
           }
                     ; return (dict', binds)
                    }
           }
@@ -1138,6 +1195,8 @@ genericNormaliseInsts isWanted fun insts
        -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
     normaliseOneInst _isWanted _fun inst
       = do { inst' <- zonkInst inst
        -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
     normaliseOneInst _isWanted _fun inst
       = do { inst' <- zonkInst inst
+           ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
+                       ppr inst
           ; return (inst', emptyBag)
           }
 \end{code}
           ; return (inst', emptyBag)
           }
 \end{code}
@@ -1156,45 +1215,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}
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)