Commit c06b46d0 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Fix #11305.

Summary:
In the fallthrough case when doing a subsumption case, we
need to deeply instantiate to remove any buried foralls in
the "actual" type.

Once this validates, please feel free to commit it; I may not
have the chance to do this on Tuesday. Back in full action on
Wed.

Test Plan: ./validate, typecheck/should_compiler/T11305

Reviewers: austin, bgamari, hvr

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1715

GHC Trac Issues: #11305
parent 34af60c7
...@@ -630,7 +630,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected ...@@ -630,7 +630,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:" do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:"
(ppr tv_a <+> text "-->" <+> ppr ty_a') (ppr tv_a <+> text "-->" <+> ppr ty_a')
; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e } ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
Unfilled _ -> mkWpCastN <$> unify } Unfilled _ -> unify }
go ty_a (TyVarTy tv_e) go ty_a (TyVarTy tv_e)
...@@ -645,33 +645,14 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected ...@@ -645,33 +645,14 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
Unfilled details Unfilled details
| canUnifyWithPolyType dflags details | canUnifyWithPolyType dflags details
&& isTouchableMetaTyVar tclvl tv_e -- don't want skolems here && isTouchableMetaTyVar tclvl tv_e -- don't want skolems here
-> mkWpCastN <$> unify -> unify
-- We've avoided instantiating ty_actual just in case ty_expected is -- We've avoided instantiating ty_actual just in case ty_expected is
-- polymorphic. But we've now assiduously determined that it is *not* -- polymorphic. But we've now assiduously determined that it is *not*
-- polymorphic. So instantiate away. This is needed for e.g. test -- polymorphic. So instantiate away. This is needed for e.g. test
-- typecheck/should_compile/T4284. -- typecheck/should_compile/T4284.
| otherwise | otherwise
-> do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual -> inst_and_unify }
-- if we haven't recurred through an arrow, then
-- the eq_orig will list ty_actual. In this case,
-- we want to update the origin to reflect the
-- instantiation. If we *have* recurred through
-- an arrow, it's better not to update.
; let eq_orig' = case eq_orig of
TypeEqOrigin { uo_actual = orig_ty_actual
, uo_expected = orig_ty_expected
, uo_thing = thing }
| orig_ty_actual `tcEqType` ty_actual
-> TypeEqOrigin
{ uo_actual = rho_a
, uo_expected = orig_ty_expected
, uo_thing = thing }
_ -> eq_orig
; cow <- uType eq_orig' TypeLevel rho_a ty_expected
; return (mkWpCastN cow <.> wrap) } }
go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res) go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
| not (isPredTy act_arg) | not (isPredTy act_arg)
...@@ -693,11 +674,37 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected ...@@ -693,11 +674,37 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
; return (body_wrap <.> in_wrap) } ; return (body_wrap <.> in_wrap) }
| otherwise -- Revert to unification | otherwise -- Revert to unification
= do { cow <- unify = inst_and_unify
; return (mkWpCastN cow) } -- It's still possible that ty_actual has nested foralls. Instantiate
-- these, as there's no way unification will succeed with them in.
-- See typecheck/should_compiler/T11350 for an example of when this
-- is important.
inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
-- if we haven't recurred through an arrow, then
-- the eq_orig will list ty_actual. In this case,
-- we want to update the origin to reflect the
-- instantiation. If we *have* recurred through
-- an arrow, it's better not to update.
; let eq_orig' = case eq_orig of
TypeEqOrigin { uo_actual = orig_ty_actual
, uo_expected = orig_ty_expected
, uo_thing = thing }
| orig_ty_actual `tcEqType` ty_actual
, not (isIdHsWrapper wrap)
-> TypeEqOrigin
{ uo_actual = rho_a
, uo_expected = orig_ty_expected
, uo_thing = thing }
_ -> eq_orig
; cow <- uType eq_orig' TypeLevel rho_a ty_expected
; return (mkWpCastN cow <.> wrap) }
-- use versions without synonyms expanded -- use versions without synonyms expanded
unify = uType eq_orig TypeLevel ty_actual ty_expected unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected
----------------- -----------------
-- needs both un-type-checked (for origins) and type-checked (for wrapping) -- needs both un-type-checked (for origins) and type-checked (for wrapping)
......
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Data.Profunctor.Strong where
import Control.Arrow
import Control.Category
import Data.Tuple
import Prelude hiding (id,(.))
infixr 0 :->
type p :-> q = forall a b. p a b -> q a b
class Profunctor p where
dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
class ProfunctorFunctor t where
promap :: Profunctor p => (p :-> q) -> t p :-> t q
class ProfunctorFunctor t => ProfunctorMonad t where
proreturn :: Profunctor p => p :-> t p
projoin :: Profunctor p => t (t p) :-> t p
class ProfunctorFunctor t => ProfunctorComonad t where
proextract :: Profunctor p => t p :-> p
produplicate :: Profunctor p => t p :-> t (t p)
class Profunctor p => Strong p where
first' :: p a b -> p (a, c) (b, c)
first' = dimap swap swap . second'
second' :: p a b -> p (c, a) (c, b)
second' = dimap swap swap . first'
----------------------------------------------------------------------------
newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
instance Profunctor p => Profunctor (Tambara p) where
dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
instance ProfunctorFunctor Tambara where
promap f (Tambara p) = Tambara (f p)
instance ProfunctorComonad Tambara where
proextract (Tambara p) = dimap (\a -> (a,())) fst p
produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
where
hither :: ((a, b), c) -> (a, (b, c))
hither ~(~(x,y),z) = (x,(y,z))
yon :: (a, (b, c)) -> ((a, b), c)
yon ~(x,~(y,z)) = ((x,y),z)
instance Profunctor p => Strong (Tambara p) where
first' = runTambara . produplicate
...@@ -486,3 +486,4 @@ test('T10971a', normal, compile, ['']) ...@@ -486,3 +486,4 @@ test('T10971a', normal, compile, [''])
test('T11237', normal, compile, ['']) test('T11237', normal, compile, [''])
test('T10592', normal, compile, ['']) test('T10592', normal, compile, [''])
test('T11254', expect_broken(11254), compile, ['']) test('T11254', expect_broken(11254), compile, [''])
test('T11305', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment