diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Rewrite.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 52 |
1 files changed, 40 insertions, 12 deletions
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 82c6c580a4..3f2f8f35ce 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -41,6 +41,8 @@ import GHC.Exts (oneShot) import Control.Monad import GHC.Utils.Monad ( zipWith3M ) import Data.List.NonEmpty ( NonEmpty(..) ) +import Control.Applicative (liftA3) +import GHC.Builtin.Types.Prim (tYPETyCon) {- ************************************************************************ @@ -470,28 +472,28 @@ rewrite_args_slow binders inner_ki fvs roles tys -- a Derived rewriting a Derived. The solution would be to generate evidence for -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also -- Note [No derived kind equalities] - = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True) + = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True) roles tys ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } where - {-# INLINE fl #-} - fl :: Bool -- must we ensure to produce a real coercion here? + {-# INLINE rw #-} + rw :: Bool -- must we ensure to produce a real coercion here? -- see comment at top of function -> Role -> Type -> RewriteM Reduction - fl True r ty = noBogusCoercions $ fl1 r ty - fl False r ty = fl1 r ty + rw True r ty = noBogusCoercions $ rw1 r ty + rw False r ty = rw1 r ty - {-# INLINE fl1 #-} - fl1 :: Role -> Type -> RewriteM Reduction - fl1 Nominal ty + {-# INLINE rw1 #-} + rw1 :: Role -> Type -> RewriteM Reduction + rw1 Nominal ty = setEqRel NomEq $ rewrite_one ty - fl1 Representational ty + rw1 Representational ty = setEqRel ReprEq $ rewrite_one ty - fl1 Phantom ty + rw1 Phantom ty -- See Note [Phantoms in the rewriter] = do { ty <- liftTcS $ zonkTcType ty ; return $ mkReflRedn Phantom ty } @@ -533,9 +535,35 @@ rewrite_one (TyConApp tc tys) rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) = do { arg_redn <- rewrite_one ty1 ; res_redn <- rewrite_one ty2 - ; w_redn <- setEqRel NomEq $ rewrite_one mult + + -- Important: look at the *reduced* type, so that any unzonked variables + -- in kinds are gone and the getRuntimeRep succeeds. + -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical. + ; let arg_rep = getRuntimeRep (reductionReducedType arg_redn) + res_rep = getRuntimeRep (reductionReducedType res_redn) + + ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $ + liftA3 (,,) (rewrite_one mult) + (rewrite_one arg_rep) + (rewrite_one res_rep) ; role <- getRole - ; return $ mkFunRedn role vis w_redn arg_redn res_redn } + + ; let arg_rep_co = reductionCoercion arg_rep_redn + -- :: arg_rep ~ arg_rep_xi + arg_ki_co = mkTyConAppCo Nominal tYPETyCon [arg_rep_co] + -- :: TYPE arg_rep ~ TYPE arg_rep_xi + casted_arg_redn = mkCoherenceRightRedn role arg_redn arg_ki_co + -- :: ty1 ~> arg_xi |> arg_ki_co + + res_rep_co = reductionCoercion res_rep_redn + res_ki_co = mkTyConAppCo Nominal tYPETyCon [res_rep_co] + casted_res_redn = mkCoherenceRightRedn role res_redn res_ki_co + + -- We must rewrite the representations, because that's what would + -- be done if we used TyConApp instead of FunTy. These rewritten + -- representations are seen only in casts of the arg and res, below. + -- Forgetting this caused #19677. + ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn } rewrite_one ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of |