[Git][ghc/ghc][master] Fixes #19627.
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu Mar 9 14:53:02 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
9ea719f2 by Apoorv Ingle at 2023-03-09T09:52:45-05:00
Fixes #19627.
Previously the solver failed with an unhelpful "solver reached too may iterations" error.
With the fix for #21909 in place we no longer have the possibility of generating such an error if we have `-fconstraint-solver-iteration` > `-fgivens-fuel > `-fwanteds-fuel`. This is true by default, and the said fix also gives programmers a knob to control how hard the solver should try before giving up.
This commit adds:
* Reference to ticket #19627 in the Note [Expanding Recursive Superclasses and ExpansionFuel]
* Test `typecheck/should_fail/T19627.hs` for regression purposes
- - - - -
4 changed files:
- compiler/GHC/Tc/Solver.hs
- + testsuite/tests/typecheck/should_fail/T19627.hs
- + testsuite/tests/typecheck/should_fail/T19627.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -2371,7 +2371,7 @@ any new unifications, and iterate the implications only if so.
-}
{- Note [Expanding Recursive Superclasses and ExpansionFuel]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the class declaration (T21909)
class C [a] => C a where
@@ -2431,7 +2431,7 @@ There are two preconditions for the default fuel values:
Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints
preferably givenFuel > wantedsFuel to avoid issues like T21909 while
the precondition (2) ensures that we do not reach the solver iteration limit and fail with a
-more meaningful error message
+more meaningful error message (see T19627)
This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.
-}
=====================================
testsuite/tests/typecheck/should_fail/T19627.hs
=====================================
@@ -0,0 +1,108 @@
+{-# language BlockArguments #-}
+{-# language DefaultSignatures #-}
+{-# language DerivingStrategies #-}
+{-# language EmptyCase #-}
+{-# language ExplicitNamespaces #-}
+{-# language ImportQualifiedPost #-}
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language FunctionalDependencies #-}
+{-# language GADTs #-}
+{-# language LambdaCase #-}
+{-# language LinearTypes #-}
+{-# language NoStarIsType #-}
+{-# language PolyKinds #-}
+{-# language QuantifiedConstraints #-}
+{-# language RankNTypes #-}
+{-# language RoleAnnotations #-}
+{-# language ScopedTypeVariables #-}
+{-# language StandaloneDeriving #-}
+{-# language StandaloneKindSignatures #-}
+{-# language StrictData #-}
+{-# language TupleSections #-}
+{-# language TypeApplications #-}
+{-# language TypeFamilies #-}
+{-# language TypeFamilyDependencies #-}
+{-# language TypeOperators #-}
+{-# language UndecidableInstances #-}
+{-# language UndecidableSuperClasses #-}
+
+module T19627 where
+
+import Data.Kind
+import Prelude hiding ( Functor(..) )
+
+--------------------
+
+class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Type) where
+ type Not p :: Type
+ (!=) :: p -> Not p -> r
+
+data Y (a :: Type) (b :: Type) (c :: Type) where
+ L :: Y a b a
+ R :: Y a b b
+
+newtype a & b = With (forall c. Y a b c -> c)
+
+with :: (forall c. Y a b c -> c) -> a & b
+with = With
+
+runWith :: a & b -> Y a b c -> c
+runWith (With f) = f
+
+withL' :: a & b -> a
+withL' (With f) = f L
+
+withR' :: a & b -> b
+withR' (With f) = f R
+
+instance (Prop a, Prop b) => Prop (a & b) where
+ type Not (a & b) = Not a `Either` Not b
+ w != Left a = withL' w != a
+ w != Right b = withR' w != b
+
+instance (Prop a, Prop b) => Prop (Either a b) where
+ type Not (Either a b) = Not a & Not b
+ Left a != w = a != withL' w
+ Right a != w = a != withR' w
+
+newtype Yoneda f a = Yoneda
+ (forall r. Prop r => (a -> r) -> f r)
+
+data Noneda f a where
+ Noneda :: Prop r => !(f r <#- (a ⊸ r)) -> Noneda f a
+
+liftYoneda :: forall f a i. (Functor f, Prop a, Iso i) => i (f a) (Yoneda f a)
+liftYoneda = iso \case
+ L -> lowerYoneda'
+ R -> lol \case
+ L -> \(Noneda ((a2r :: a ⊸ r) :-#> nfr)) -> runLol (fmap @f @a @r a2r) L nfr
+ R -> \fa -> Yoneda do
+ lol \case
+ R -> \f -> fmap' f fa
+ L -> \nfr -> whyNot \a2r -> fmap a2r fa != nfr
+
+
+type family NotApart (p :: Type -> Type -> Type) :: Type -> Type -> Type
+
+class
+ ( forall a b. (Prop a, Prop b) => Prop (p a b)
+ , NotApart (NotIso p) ~ p
+ ) => Iso p where
+ type NotIso p = (q :: Type -> Type -> Type) | q -> p
+ iso :: (forall c. Y (b ⊸ a) (a ⊸ b) c -> c) -> p a b
+
+data b <#- a where (:-#>) :: a -> Not b -> b <#- a
+newtype a ⊸ b = Lol (forall c. Y (Not b %1 -> Not a) (a %1 -> b) c -> c)
+
+class
+ ( forall a. Prop a => Prop (f a)
+ ) => Functor f where
+ fmap' :: (Prop a, Prop b, Lol l, Lol l') => l ((a ⊸ b)) (l' (f a) (f b))
+
+fmap :: forall f a b l. (Functor f, Prop a, Prop b, Lol l) => (a ⊸ b) -> l (f a) (f b)
+fmap f = fmap' f
+
+class Iso p => Lol (p :: Type -> Type -> Type) where
+ lol :: (forall c. Y (Not b -> Not a) (a -> b) c -> c) -> p a b
+ apartR :: Not (p a b) -> b <#- a
=====================================
testsuite/tests/typecheck/should_fail/T19627.stderr
=====================================
@@ -0,0 +1,45 @@
+
+T19627.hs:108:3: error: [GHC-05617]
+ • Could not deduce ‘Not (p0 a b) ~ Not (p a b)’
+ from the context: Lol p
+ bound by the type signature for:
+ apartR :: forall (p :: * -> * -> *) a b.
+ Lol p =>
+ Not (p a b) -> b <#- a
+ at T19627.hs:108:3-34
+ Expected: Not (p a b) -> b <#- a
+ Actual: Not (p0 a b) -> b <#- a
+ NB: ‘Not’ is a non-injective type family
+ The type variable ‘p0’ is ambiguous
+ • In the ambiguity check for ‘apartR’
+ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+ When checking the class method:
+ apartR :: forall (p :: * -> * -> *) a b.
+ Lol p =>
+ Not (p a b) -> b <#- a
+ In the class declaration for ‘Lol’
+
+T19627.hs:108:3: error: [GHC-05617]
+ • Could not deduce ‘Not (Not (p0 a1 b1)) ~ p0 a1 b1’
+ arising from a superclass required to satisfy ‘Prop (p0 a1 b1)’,
+ arising from the head of a quantified constraint
+ arising from a superclass required to satisfy ‘Iso p0’,
+ arising from a superclass required to satisfy ‘Lol p0’,
+ arising from a type ambiguity check for
+ the type signature for ‘apartR’
+ from the context: Lol p
+ bound by the type signature for:
+ apartR :: forall (p :: * -> * -> *) a b.
+ Lol p =>
+ Not (p a b) -> b <#- a
+ at T19627.hs:108:3-34
+ or from: (Prop a1, Prop b1)
+ bound by a quantified context at T19627.hs:108:3-34
+ The type variable ‘p0’ is ambiguous
+ • In the ambiguity check for ‘apartR’
+ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+ When checking the class method:
+ apartR :: forall (p :: * -> * -> *) a b.
+ Lol p =>
+ Not (p a b) -> b <#- a
+ In the class declaration for ‘Lol’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -671,3 +671,4 @@ test('T20666a', normal, compile, ['']) # To become compile_fail after migration
test('T22924a', normal, compile_fail, [''])
test('T22924b', normal, compile_fail, [''])
test('T22940', normal, compile_fail, [''])
+test('T19627', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9ea719f2f1929bf2b789e4001f6c542a04185d61
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9ea719f2f1929bf2b789e4001f6c542a04185d61
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230309/a4a4bbe9/attachment-0001.html>
More information about the ghc-commits
mailing list