[commit: ghc] wip/rae: Fix #11305. (718ab6d)
git at git.haskell.org
git at git.haskell.org
Wed Dec 30 03:12:12 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/rae
Link : http://ghc.haskell.org/trac/ghc/changeset/718ab6d8644e21dbc36f42c9bada788a8ca2b6af/ghc
>---------------------------------------------------------------
commit 718ab6d8644e21dbc36f42c9bada788a8ca2b6af
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Tue Dec 29 00:27:59 2015 -0500
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
>---------------------------------------------------------------
718ab6d8644e21dbc36f42c9bada788a8ca2b6af
compiler/typecheck/TcUnify.hs | 57 ++++++++++++----------
testsuite/tests/typecheck/should_compile/T11305.hs | 57 ++++++++++++++++++++++
testsuite/tests/typecheck/should_compile/all.T | 1 +
3 files changed, 90 insertions(+), 25 deletions(-)
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b7bc77d..908b692 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -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:"
(ppr tv_a <+> text "-->" <+> ppr ty_a')
; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
- Unfilled _ -> mkWpCastN <$> unify }
+ Unfilled _ -> unify }
go ty_a (TyVarTy tv_e)
@@ -645,33 +645,14 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
Unfilled details
| canUnifyWithPolyType dflags details
&& isTouchableMetaTyVar tclvl tv_e -- don't want skolems here
- -> mkWpCastN <$> unify
+ -> unify
-- We've avoided instantiating ty_actual just in case ty_expected is
-- polymorphic. But we've now assiduously determined that it is *not*
-- polymorphic. So instantiate away. This is needed for e.g. test
-- typecheck/should_compile/T4284.
| otherwise
- -> 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
- -> 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) } }
+ -> inst_and_unify }
go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
| not (isPredTy act_arg)
@@ -693,11 +674,37 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
; return (body_wrap <.> in_wrap) }
| otherwise -- Revert to unification
- = do { cow <- unify
- ; return (mkWpCastN cow) }
+ = inst_and_unify
+ -- 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
- 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)
diff --git a/testsuite/tests/typecheck/should_compile/T11305.hs b/testsuite/tests/typecheck/should_compile/T11305.hs
new file mode 100644
index 0000000..14cb955
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T11305.hs
@@ -0,0 +1,57 @@
+{-# 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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 20ef3a7..3fa1f8c 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -486,3 +486,4 @@ test('T10971a', normal, compile, [''])
test('T11237', normal, compile, [''])
test('T10592', normal, compile, [''])
test('T11254', expect_broken(11254), compile, [''])
+test('T11305', normal, compile, [''])
More information about the ghc-commits
mailing list