Fix #13819 by refactoring TypeEqOrigin.uo_thing
[ghc.git] / compiler / typecheck / TcUnify.hs
index ef0c95a..e09b5bf 100644 (file)
@@ -16,7 +16,7 @@ module TcUnify (
   checkConstraints, buildImplicationFor,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind, noThing,
+  unifyType, unifyTheta, unifyKind,
   uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
@@ -59,7 +59,6 @@ import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Name   ( Name )
 import Bag
 import Util
 import Pair( pFst )
@@ -138,7 +137,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; return (result, idHsWrapper) }
 
     go acc_arg_tys n ty
-      | Just ty' <- coreView ty = go acc_arg_tys n ty'
+      | Just ty' <- tcView ty = go acc_arg_tys n ty'
 
     go acc_arg_tys n (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
@@ -202,10 +201,9 @@ matchExpectedFunTys herald arity orig_ty thing_inside
 
 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
 -- for example in function application
-matchActualFunTys :: Outputable a
-                  => SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                   -> CtOrigin
-                  -> Maybe a   -- the thing with type TcSigmaType
+                  -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
                   -> Arity
                   -> TcSigmaType
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
@@ -216,10 +214,9 @@ matchActualFunTys herald ct_orig mb_thing arity ty
 
 -- | Variant of 'matchActualFunTys' that works when supplied only part
 -- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart :: Outputable a
-                      => SDoc -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
                       -> CtOrigin
-                      -> Maybe a  -- the thing with type TcSigmaType
+                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
                       -> Arity
                       -> TcSigmaType
                       -> [TcSigmaType] -- reversed args. See (*) below.
@@ -269,7 +266,7 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
         (tvs, theta, _) = tcSplitSigmaTy ty
 
     go n acc_args ty
-      | Just ty' <- coreView ty = go n acc_args ty'
+      | Just ty' <- tcView ty = go n acc_args ty'
 
     go n acc_args (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
@@ -370,7 +367,7 @@ matchExpectedTyConApp tc orig_ty
   = ASSERT(tc /= funTyCon) go orig_ty
   where
     go ty
-       | Just ty' <- coreView ty
+       | Just ty' <- tcView ty
        = go ty'
 
     go ty@(TyConApp tycon args)
@@ -401,7 +398,7 @@ matchExpectedTyConApp tc orig_ty
            ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
            ; let args = mkTyVarTys arg_tvs
                  tc_template = mkTyConApp tc args
-           ; co <- unifyType noThing tc_template orig_ty
+           ; co <- unifyType Nothing tc_template orig_ty
            ; return (co, args) }
 
 ----------------------
@@ -415,7 +412,7 @@ matchExpectedAppTy orig_ty
   = go orig_ty
   where
     go ty
-      | Just ty' <- coreView ty = go ty'
+      | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
       = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
@@ -433,7 +430,7 @@ matchExpectedAppTy orig_ty
     defer
       = do { ty1 <- newFlexiTyVarTy kind1
            ; ty2 <- newFlexiTyVarTy kind2
-           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
+           ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
     orig_kind = typeKind orig_ty
@@ -532,9 +529,8 @@ skolemising the type.
 
 -- | Call this variant when you are in a higher-rank situation and
 -- you know the right-hand type is deeply skolemised.
-tcSubTypeHR :: Outputable a
-            => CtOrigin    -- ^ of the actual type
-            -> Maybe a     -- ^ If present, it has type ty_actual
+tcSubTypeHR :: CtOrigin               -- ^ of the actual type
+            -> Maybe (HsExpr GhcRn)   -- ^ If present, it has type ty_actual
             -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
@@ -567,7 +563,7 @@ tcSubTypeO orig ctxt ty_actual ty_expected
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -614,12 +610,11 @@ tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWr
 tcSubTypeDS orig ctxt ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
-tcSubTypeDS_NC_O :: Outputable a
-                 => CtOrigin   -- origin used for instantiation only
+tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
                  -> UserTypeCtxt
-                 -> Maybe a
+                 -> Maybe (HsExpr GhcRn)
                  -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
@@ -629,7 +624,7 @@ tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
       Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
          where
            eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
-                                  , uo_thing = mkErrorThing <$> m_thing }
+                                  , uo_thing  = ppr <$> m_thing }
 
 ---------------
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
@@ -638,8 +633,8 @@ tc_sub_tc_type :: CtOrigin   -- used when calling uType
 -- If wrap = tc_sub_type t1 t2
 --    => wrap :: t1 ~> t2
 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
-  | is_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
-  , not (is_poly ty_actual)
+  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
+  , not (possibly_poly ty_actual)
   = do { traceTc "tc_sub_tc_type (drop to equality)" $
          vcat [ text "ty_actual   =" <+> ppr ty_actual
               , text "ty_expected =" <+> ppr ty_expected ]
@@ -656,13 +651,21 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
                                                  ty_actual sk_rho
        ; return (sk_wrap <.> inner_wrap) }
   where
-    is_poly ty
+    possibly_poly ty
       | isForAllTy ty                        = True
-      | Just (_, res) <- splitFunTy_maybe ty = is_poly res
+      | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
       | otherwise                            = False
       -- NB *not* tcSplitFunTy, because here we want
       -- to decompose type-class arguments too
 
+    definitely_poly ty
+      | (tvs, theta, tau) <- tcSplitSigmaTy ty
+      , (tv:_) <- tvs
+      , null theta
+      , isInsolubleOccursCheck NomEq tv tau
+      = True
+      | otherwise
+      = False
 
 {- Note [Don't skolemise unnecessarily]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -674,11 +677,31 @@ error.  It's better to say that
     (Char->Char) ~ (forall a. a->a)
 fails.
 
-In general,
- * if the RHS type an outermost forall (i.e. skolemisation
-   is the next thing we'd do)
- * and the LHS has no top-level polymorphism (but looking deeply)
-then we can revert to simple equality.
+So roughly:
+ * if the ty_expected has an outermost forall
+      (i.e. skolemisation is the next thing we'd do)
+ * and the ty_actual has no top-level polymorphism (but looking deeply)
+then we can revert to simple equality.  But we need to be careful.
+These examples are all fine:
+
+ * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
+      Polymorphism is buried in ty_actual
+
+ * (Char->Char) <= (forall a. Char -> Char)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. (a~Char) => a -> a)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. F [a] Char -> Char)
+                   where type instance F [x] t = t
+     ty_expected isn't really polymorphic
+
+If we prematurely go to equality we'll reject a program we should
+accept (e.g. Trac #13752).  So the test (which is only to improve
+error message) is very conservative:
+ * ty_actual is /definitely/ monomorphic
+ * ty_expected is /definitely/ polymorphic
 -}
 
 ---------------
@@ -695,8 +718,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
               , text "ty_expected =" <+> ppr ty_expected ]
        ; go ty_actual ty_expected }
   where
-    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
-                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
 
     go (TyVarTy tv_a) ty_e
       = do { lookup_res <- lookupTcTyVar tv_a
@@ -772,19 +795,19 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
 -- expressions
-tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-             -> TcM (HsExpr TcId)
-tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
+tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+             -> TcM (HsExpr GhcTcId)
+tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
 
 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
 -- convenient.
-tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-               -> TcM (HsExpr TcId)
-tcWrapResultO orig expr actual_ty res_ty
+tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+               -> TcM (HsExpr GhcTcId)
+tcWrapResultO orig rn_expr expr actual_ty res_ty
   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                       , text "Expected:" <+> ppr res_ty ])
        ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
-                                 (Just expr) actual_ty res_ty
+                                 (Just rn_expr) actual_ty res_ty
        ; return (mkHsWrap cow expr) }
 
 -----------------------------------
@@ -873,7 +896,7 @@ In some cases we want to deeply instantiate before filling in
 an InferResult, and in some cases not.  That's why InferReult
 has the ir_inst flag.
 
-* ir_inst = True: deeply instantantiate
+* ir_inst = True: deeply instantiate
 
   Consider
     f x = (*)
@@ -893,7 +916,7 @@ has the ir_inst flag.
   Here want to instantiate f's type so that the ?x::Int constraint
   gets discharged by the enclosing implicit-parameter binding.
 
-* ir_inst = False: do not instantantiate
+* ir_inst = False: do not instantiate
 
   Consider this (which uses visible type application):
 
@@ -1157,30 +1180,26 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
-unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
+unifyType :: Maybe (HsExpr GhcRn)   -- ^ If present, has type 'ty1'
           -> TcTauType -> TcTauType -> TcM TcCoercionN
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
-unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
+unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType origin TypeLevel ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
-                          , uo_thing  = mkErrorThing <$> thing }
-
--- | Use this instead of 'Nothing' when calling 'unifyType' without
--- a good "thing" (where the "thing" has the "actual" type passed in)
--- This has an 'Outputable' instance, avoiding amgiguity problems.
-noThing :: Maybe (HsExpr Name)
-noThing = Nothing
+                          , uo_thing  = ppr <$> thing }
 
-unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
-unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
+unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
+unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType origin KindLevel ty1 ty2
   where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
-                              , uo_thing  = mkErrorThing <$> thing }
+                              , uo_thing  = ppr <$> thing }
 
 ---------------
 unifyPred :: PredType -> PredType -> TcM TcCoercionN
 -- Actual and expected types
-unifyPred = unifyType noThing
+unifyPred = unifyType Nothing
 
 ---------------
 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
@@ -1273,8 +1292,8 @@ uType origin t_or_k orig_ty1 orig_ty2
         -- we'll end up saying "can't match Foo with Bool"
         -- rather than "can't match "Int with Bool".  See Trac #4535.
     go ty1 ty2
-      | Just ty1' <- coreView ty1 = go ty1' ty2
-      | Just ty2' <- coreView ty2 = go ty1  ty2'
+      | Just ty1' <- tcView ty1 = go ty1' ty2
+      | Just ty2' <- tcView ty2 = go ty1  ty2'
 
     go (CastTy t1 co1) t2
       = do { co_tys <- go t1 t2
@@ -1299,7 +1318,7 @@ uType origin t_or_k orig_ty1 orig_ty2
 
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
-      | tc1 == tc2, length tys1 == length tys2
+      | tc1 == tc2, equalLength tys1 tys2
       = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
         do { cos <- zipWithM (uType origin t_or_k) tys1 tys2
            ; return $ mkTyConAppCo Nominal tc1 cos }
@@ -1500,11 +1519,16 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
       = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1)
-           ; co   <- updateMeta tv1 ty2' co_k
-           ; return (maybe_sym swapped co) }
+           ; if isTcReflCo co_k  -- only proceed if the kinds matched.
+
+             then do { writeMetaTyVar tv1 ty2'
+                     ; return (mkTcNomReflCo ty2') }
+             else defer } -- this cannot be solved now.
+                          -- See Note [Equalities with incompatible kinds]
+                          -- in TcCanonical
 
       | otherwise
-      = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
+      = defer
                -- Occurs check or an untouchable: just defer
                -- NB: occurs check isn't necessarily fatal:
                --     eg tv1 occured in type family parameter
@@ -1512,10 +1536,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     ty1 = mkTyVarTy tv1
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
 
--- | apply sym iff swapped
-maybe_sym :: SwapFlag -> Coercion -> Coercion
-maybe_sym IsSwapped  = mkSymCo
-maybe_sym NotSwapped = id
+    defer = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
 swapOverTyVars tv1 tv2
@@ -1573,7 +1594,6 @@ canSolveByUnification tclvl tv xi
                                         SigTv -> True
                                         _     -> False
                        SkolemTv {} -> True
-                       FlatSkol {} -> False
                        RuntimeUnk  -> True
 
 {- Note [Fmv Orientation Invariant]
@@ -1740,18 +1760,6 @@ lookupTcTyVar tyvar
   where
     details = tcTyVarDetails tyvar
 
--- | Fill in a meta-tyvar
-updateMeta :: TcTyVar            -- ^ tv to fill in, tv :: k1
-           -> TcType             -- ^ ty2 :: k2
-           -> Coercion           -- ^ kind_co :: k2 ~N k1
-           -> TcM Coercion       -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
-updateMeta tv1 ty2 kind_co
-  = do { let ty2'     = ty2 `mkCastTy` kind_co
-             ty2_refl = mkNomReflCo ty2
-             co       = mkCoherenceLeftCo ty2_refl kind_co
-       ; writeMetaTyVar tv1 ty2'
-       ; return co }
-
 {-
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1761,14 +1769,14 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Arity           -- ^ # of args remaining, only for errors
-                     -> TcType          -- ^ type, only for errors
+matchExpectedFunKind :: Outputable fun
+                     => fun             -- ^ type, only for errors
                      -> TcKind          -- ^ function kind
                      -> TcM (Coercion, TcKind, TcKind)
                                   -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind num_args_remaining ty = go
+matchExpectedFunKind hs_ty = go
   where
-    go k | Just k' <- coreView k = go k'
+    go k | Just k' <- tcView k = go k'
 
     go k@(TyVarTy kvar)
       | isTcTyVar kvar, isMetaTyVar kvar
@@ -1784,10 +1792,9 @@ matchExpectedFunKind num_args_remaining ty = go
       = do { arg_kind <- newMetaKindVar
            ; res_kind <- newMetaKindVar
            ; let new_fun = mkFunTy arg_kind res_kind
-                 thing   = mkTypeErrorThingArgs ty num_args_remaining
                  origin  = TypeEqOrigin { uo_actual   = k
                                         , uo_expected = new_fun
-                                        , uo_thing    = Just thing
+                                        , uo_thing    = Just (ppr hs_ty)
                                         }
            ; co <- uType origin KindLevel k new_fun
            ; return (co, arg_kind, res_kind) }
@@ -2040,8 +2047,8 @@ occCheckExpand tv ty
     go env ty@(TyConApp tc tys)
       = case mapM (go env) tys of
           Just tys' -> return (mkTyConApp tc tys')
-          Nothing | Just ty' <- coreView ty -> go env ty'
-                  | otherwise               -> Nothing
+          Nothing | Just ty' <- tcView ty -> go env ty'
+                  | otherwise             -> Nothing
                       -- Failing that, try to expand a synonym
 
     go env (CastTy ty co) =  do { ty' <- go env ty