diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2022-05-13 11:34:25 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-07-25 09:42:01 -0400 |
commit | dc27e15a76486b1ebd27a77f8515044c2671e22d (patch) | |
tree | 046a9d5f4ea9b3f72e533fde1bff8dba7c4461a7 /testsuite/tests/typecheck | |
parent | ce0cd12c65b4130dc6eb9952e058828d65d8a2ad (diff) | |
download | haskell-dc27e15a76486b1ebd27a77f8515044c2671e22d.tar.gz |
Implement DeepSubsumption
This MR adds the language extension -XDeepSubsumption, implementing
GHC proposal #511. This change mitigates the impact of GHC proposal
The changes are highly localised, by design. See Note [Deep subsumption]
in GHC.Tc.Utils.Unify.
The main changes are:
* Add -XDeepSubsumption, which is on by default in Haskell98 and Haskell2010,
but off in Haskell2021.
-XDeepSubsumption largely restores the behaviour before the "simple subsumption" change.
-XDeepSubsumpition has a similar flavour as -XNoMonoLocalBinds:
it makes type inference more complicated and less predictable, but it
may be convenient in practice.
* The main changes are in:
* GHC.Tc.Utils.Unify.tcSubType, which does deep susumption and eta-expanansion
* GHC.Tc.Utils.Unify.tcSkolemiseET, which does deep skolemisation
* In GHC.Tc.Gen.App.tcApp we call tcSubTypeNC to match the result
type. Without deep subsumption, unifyExpectedType would be sufficent.
See Note [Deep subsumption] in GHC.Tc.Utils.Unify.
* There are no changes to Quick Look at all.
* The type of `withDict` becomes ambiguous; so add -XAllowAmbiguousTypes to
GHC.Magic.Dict
* I fixed a small but egregious bug in GHC.Core.FVs.varTypeTyCoFVs, where
we'd forgotten to take the free vars of the multiplicity of an Id.
* I also had to fix tcSplitNestedSigmaTys
When I did the shallow-subsumption patch
commit 2b792facab46f7cdd09d12e79499f4e0dcd4293f
Date: Sun Feb 2 18:23:11 2020 +0000
Simple subsumption
I changed tcSplitNestedSigmaTys to not look through function arrows
any more. But that was actually an un-forced change. This function
is used only in
* Improving error messages in GHC.Tc.Gen.Head.addFunResCtxt
* Validity checking for default methods: GHC.Tc.TyCl.checkValidClass
* A couple of calls in the GHCi debugger: GHC.Runtime.Heap.Inspect
All to do with validity checking and error messages. Acutally its
fine to look under function arrows here, and quite useful a test
DeepSubsumption05 (a test motivated by a build failure in the
`lens` package) shows.
The fix is easy. I added Note [tcSplitNestedSigmaTys].
Diffstat (limited to 'testsuite/tests/typecheck')
8 files changed, 161 insertions, 5 deletions
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs new file mode 100644 index 0000000000..d07525b7eb --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeepSubsumption #-} +module Repro where + +import GHC.Generics +import Data.Binary + +data FFIType + = FFIVoid + deriving (Show, Generic, Binary) diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs new file mode 100644 index 0000000000..fe8be78f38 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE BangPatterns, Rank2Types, FlexibleContexts, LambdaCase, DeepSubsumption #-} +module DeepSubsumption02 where + +import Data.Semigroup + +-- | Finite source +type Source r s = Tap r (Maybe s) + +newtype Sink t m a = Sink + { unSink :: forall r. t m -> (a -> t m -> m r) -> m r } + +-- | Mono in/out +type Converter p q r s m = Source r s (Sink (Source p q) m) + +type Pipe a b m = forall r. (Monoid r, Semigroup r) => Converter r a r b m + +newtype Tap r s m = Tap { unTap :: r -> m (s, Tap r s m) } + +type Distiller tap r s m = Tap r s (Sink tap m) + +filter :: Monad m => (a -> Bool) -> Pipe a a m +--filter f = filtering $ maybe True f +filter = filtering . maybe True +{-# INLINE filter #-} + +mapAccum :: Monad m => (s -> a -> (s, b)) -> s -> Pipe a b m +--mapAccum f x = go x where +mapAccum f = go where + go s = reservingTap $ \case + Just a -> let (s', b) = f s a in return (Just b, go s') + Nothing -> return (Nothing, go s) +{-# INLINE mapAccum #-} + +traverse :: (Monad m) => (a -> m b) -> Pipe a b m +-- traverse f = traversing $ Prelude.traverse f +traverse = traversing . Prelude.traverse +{-# INLINE traverse #-} + +-- | Get one element preserving a request +reservingTap :: Monad m => (a -> Sink (Tap r a) m (b, Distiller (Tap r a) r b m)) -> Distiller (Tap r a) r b m +reservingTap k = Tap $ \r -> Sink $ \t cont -> do + (a, t') <- unTap t r + unSink (k a) t' cont +{-# INLINE reservingTap #-} + +traversing :: (Monad m) => (a -> m b) -> Distiller (Tap r a) r b m +traversing f = go where + go = reservingTap $ \a -> do + b <- undefined $ f a + return (b, go) +{-# INLINE traversing #-} + +filtering :: (Monoid r, Monad m) => (a -> Bool) -> Distiller (Tap r a) r a m +filtering f = go where + go = reservingTap $ \a -> if f a + then return (a, go) + else unTap go mempty +{-# INLINE filtering #-} + +instance Functor (Sink s m) where + fmap f m = Sink $ \s k -> unSink m s (k . f) + +instance Applicative (Sink s m) where + pure a = Sink $ \s k -> k a s + Sink mf <*> Sink mx = Sink + $ \s k -> mf s $ \f s' -> mx s' $ k . f + m *> k = m >>= \_ -> k + +instance Monad (Sink s m) where + return = pure + {-# INLINE return #-} + m >>= k = Sink $ \s cont -> unSink m s $ \a s' -> unSink (k a) s' cont + diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs new file mode 100644 index 0000000000..8f8c465047 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE DeepSubsumption #-} +{-# LANGUAGE NoPolyKinds #-} +module DeepSubsumption03 where + +class Profunctor p where + dimap :: (s -> a) -> (b -> t) -> p i a b -> p i s t + +type Iso s t a b = forall p i . Profunctor p => p i a b -> p i s t + +iso :: (s -> a) -> (b -> t) -> Iso s t a b +-- iso f g = dimap f g +iso = dimap diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs new file mode 100644 index 0000000000..abaf8d569b --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DeepSubsumption #-} +{-# LANGUAGE KindSignatures #-} +module DeepSubsumption04 where + +import Data.Kind + +data TermOutput = TermOutput + +type TermAction = () -> TermOutput + +type ActionT = WriterT TermAction + +class MonadReader r m where + ask :: m r + +data WriterT w (m :: Type -> Type) a = WriterT + +type ActionM a = forall m . (MonadReader () m) => ActionT m a + +output :: TermAction -> ActionM () +output t = undefined + +termText :: String -> TermOutput +termText = undefined + +outputText :: String -> ActionM () +outputText = output . const . termText +--outputText x = output . const . termText $ x + diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs new file mode 100644 index 0000000000..a6d9db3cb9 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DeepSubsumption #-} +module DeepSubsumption06 where + +type Traversal' s a = forall f . Applicative f => (a -> a) -> f s -> f s +type LensLike f m a = (a -> a) -> f m -> f m + +class Ixed m where + ix :: () -> Traversal' m () + + default ix :: (Applicative f) => () -> LensLike f m () + ix = undefined diff --git a/testsuite/tests/typecheck/should_compile/T21548a.hs b/testsuite/tests/typecheck/should_compile/T21548a.hs new file mode 100644 index 0000000000..399f3e5386 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T21548a.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE RankNTypes, DeepSubsumption #-} + +module T21548a where + +f1 :: (forall a. a -> forall b. b -> b) -> Int +f1 = f1 + +g1 :: forall p q. p -> q -> q +g1 = g1 + +foo1 = f1 g1 + diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 62edaf99e6..3410ad68bb 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -843,3 +843,9 @@ test('T18802', normal, compile, ['']) test('T18802b', normal, compile, ['']) test('T21289', normal, compile, ['']) test('HardRecordUpdate', normal, compile, ['']) +test('T21548a', normal, compile, ['']) +test('DeepSubsumption01', normal, compile, ['']) +test('DeepSubsumption02', normal, compile, ['']) +test('DeepSubsumption03', normal, compile, ['']) +test('DeepSubsumption04', normal, compile, ['']) +test('DeepSubsumption05', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T14618.stderr b/testsuite/tests/typecheck/should_fail/T14618.stderr index 05a763048e..6cf768bbce 100644 --- a/testsuite/tests/typecheck/should_fail/T14618.stderr +++ b/testsuite/tests/typecheck/should_fail/T14618.stderr @@ -1,10 +1,10 @@ T14618.hs:7:14: error: - • Couldn't match type ‘b’ with ‘forall c. a’ - Expected: a -> b - Actual: a -> forall c. a - Cannot equate type variable ‘b’ - with a type involving polytypes: forall c. a + • Couldn't match expected type ‘b’ with actual type ‘a’ + ‘a’ is a rigid type variable bound by + the type signature for: + safeCoerce :: forall a b. a -> b + at T14618.hs:6:1-20 ‘b’ is a rigid type variable bound by the type signature for: safeCoerce :: forall a b. a -> b |