summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Solver')
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs5
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs52
2 files changed, 42 insertions, 15 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index e8c4ee82e2..cdb86b92e2 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -914,7 +914,6 @@ track whether or not we've already rewritten.
It is conceivable to do a better job at tracking whether or not a type
is rewritten, but this is left as future work. (Mar '15)
-
Note [Decomposing FunTy]
~~~~~~~~~~~~~~~~~~~~~~~~
can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This
@@ -1291,8 +1290,8 @@ zonk_eq_types = go
split2 = tcSplitFunTy_maybe ty2
go ty1 ty2
- | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1
- , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2
+ | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
+ , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
= if tc1 == tc2 && tys1 `equalLength` tys2
-- Crucial to check for equal-length args, because
-- we cannot assume that the two args to 'go' have
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