TcUnify.subFunTys must take type families into account
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 17 Oct 2007 11:43:26 +0000 (11:43 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 17 Oct 2007 11:43:26 +0000 (11:43 +0000)
* A bug reported by Andrew Appleyard revealed that subFunTys did take
  neither type families nor equalities into account.  In a fairly obscure
  case there was also a coercion ignored.

compiler/hsSyn/HsUtils.lhs
compiler/typecheck/TcUnify.lhs

index e9d80c0..d30cd1b 100644 (file)
@@ -88,12 +88,16 @@ mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
 
 mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
 mkHsWrap co_fn e | isIdHsWrapper co_fn = e
-                | otherwise          = HsWrap co_fn e
+                | otherwise           = HsWrap co_fn e
 
 mkHsWrapCoI :: CoercionI -> HsExpr id -> HsExpr id
 mkHsWrapCoI IdCo     e = e
 mkHsWrapCoI (ACo co) e = mkHsWrap (WpCo co) e
 
+coiToHsWrapper :: CoercionI -> HsWrapper
+coiToHsWrapper IdCo     = idHsWrapper
+coiToHsWrapper (ACo co) = WpCo co
+
 mkHsLam :: [LPat id] -> LHsExpr id -> LHsExpr id
 mkHsLam pats body = mkHsPar (L (getLoc body) (HsLam matches))
        where
index 29aa61a..6b8f2b3 100644 (file)
@@ -128,7 +128,8 @@ subFunTys error_herald n_pats res_ty thing_inside
 
     loop n args_so_far res_ty
        | isSigmaTy res_ty      -- Do this before checking n==0, because we 
-                               -- guarantee to return a BoxyRhoType, not a BoxySigmaType
+                               -- guarantee to return a BoxyRhoType, not a 
+                                -- BoxySigmaType
        = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
                                         loop n args_so_far res_ty'
             ; return (gen_fn <.> co_fn, res) }
@@ -142,18 +143,31 @@ subFunTys error_herald n_pats res_ty thing_inside
             ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
             ; return (co_fn', res) }
 
+        -- Try to normalise synonym families and defer if that's not possible
+    loop n args_so_far ty@(TyConApp tc tys)
+        | isOpenSynTyCon tc
+        = do { (coi1, ty') <- tcNormaliseFamInst ty
+             ; case coi1 of
+                IdCo   -> defer    -- no progress, but maybe solvable => defer
+                 ACo _  ->          -- progress: so lets try again
+                  do { (co_fn, res) <- loop n args_so_far ty'
+                     ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
+                     }
+             }
+
        -- res_ty might have a type variable at the head, such as (a b c),
        -- in which case we must fill in with (->).  Simplest thing to do
        -- is to use boxyUnify, but we catch failure and generate our own
        -- error message on failure
     loop n args_so_far res_ty@(AppTy _ _)
        = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
-            ; (_, mb_coi) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+            ; (_, mb_coi) <- tryTcErrs $ 
+                                boxyUnify res_ty (FunTy arg_ty' res_ty')
             ; if isNothing mb_coi then bale_out args_so_far
-              else do { case expectJust "subFunTys" mb_coi of
-                               IdCo -> return ()
-                               ACo co -> traceTc (text "you're dropping a coercion: " <+> ppr co)
-                      ; loop n args_so_far (FunTy arg_ty' res_ty') 
+              else do { let coi = expectJust "subFunTys" mb_coi
+                      ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty' 
+                                                                   res_ty')
+                       ; return (co_fn <.> coiToHsWrapper coi, res)
                       }
             }
 
@@ -162,9 +176,13 @@ subFunTys error_herald n_pats res_ty thing_inside
        = do { cts <- readMetaTyVar tv 
             ; case cts of
                 Indirect ty -> loop n args_so_far ty
-                Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
-                            ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
-                            ; return (idHsWrapper, res) } }
+                Flexi -> 
+                   do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+                     ; res <- thing_inside (reverse args_so_far ++ arg_tys) 
+                                            res_ty
+                     ; return (idHsWrapper, res) } }
+        | otherwise             -- defer as tyvar may be refined by equalities
+        = defer
        where
          mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
          mk_res_ty [] = panic "TcUnify.mk_res_ty1"
@@ -174,6 +192,18 @@ subFunTys error_herald n_pats res_ty thing_inside
 
     loop n args_so_far res_ty = bale_out args_so_far
 
+         -- build a template type a1 -> ... -> an -> b and defer an equality
+         -- between that template and the expected result type res_ty; then,
+         -- use the template to type the thing_inside
+    defer
+      = do { arg_tys <- newFlexiTyVarTys n_pats argTypeKind
+           ; res_ty' <- newFlexiTyVarTy openTypeKind
+           ; let fun_ty = mkFunTys arg_tys res_ty'
+           ; coi <- defer_unification False False fun_ty res_ty
+           ; res <- thing_inside arg_tys res_ty'
+           ; return (coiToHsWrapper coi, res)
+           }
+
     bale_out args_so_far 
        = do { env0 <- tcInitTidyEnv
             ; res_ty' <- zonkTcType res_ty
@@ -719,9 +749,7 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
        ; traceTc (case coi of 
                        IdCo   -> text "tc_sub1 (Rule SBOXY) IdCo"
                        ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
-       ; return $ case coi of
-                       IdCo   -> idHsWrapper 
-                       ACo co -> WpCo co
+       ; return $ coiToHsWrapper coi
        }
 
 -----------------------------------
@@ -833,9 +861,7 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
 defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
   = do { coi <- addSubCtxt sub_ctxt act_sty exp_sty $
          u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
-       ; return $ case coi of
-                       IdCo   -> idHsWrapper 
-                       ACo co -> WpCo co
+       ; return $ coiToHsWrapper coi
        }
   where
     outer = case sub_ctxt of           -- Ugh