diff options
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 55 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T23171.hs | 43 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
3 files changed, 79 insertions, 20 deletions
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index db546edfd4..845e954b83 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -2394,22 +2394,32 @@ has a separate call to isStuckTypeFamily, so the `F` above will still be accepte -} +-- | Why was the LHS 'PatersonSize' not strictly smaller than the RHS 'PatersonSize'? +-- +-- See Note [Paterson conditions] in GHC.Tc.Validity. data PatersonSizeFailure - = PSF_TyFam TyCon -- Type family - | PSF_Size -- Too many type constructors/variables - | PSF_TyVar [TyVar] -- These type variables appear more often than in instance head; - -- no duplicates in this list + -- | Either side contains a type family. + = PSF_TyFam TyCon + -- | The size of the LHS is not strictly less than the size of the RHS. + | PSF_Size + -- | These type variables appear more often in the LHS than in the RHS. + | PSF_TyVar [TyVar] -- ^ no duplicates in this list -------------------------------------- -data PatersonSize -- See Note [Paterson conditions] in GHC.Tc.Validity - = PS_TyFam TyCon -- Mentions a type family; infinite size - - | PS_Vanilla { ps_tvs :: [TyVar] -- Free tyvars, including repetitions; - , ps_size :: Int -- Number of type constructors and variables +-- | The Paterson size of a given type, in the sense of +-- Note [Paterson conditions] in GHC.Tc.Validity +-- +-- - after expanding synonyms, +-- - ignoring coercions (as they are not user written). +data PatersonSize + -- | The type mentions a type family, so the size could be anything. + = PS_TyFam TyCon + + -- | The type does not mention a type family. + | PS_Vanilla { ps_tvs :: [TyVar] -- ^ free tyvars, including repetitions; + , ps_size :: Int -- ^ number of type constructors and variables } - -- Always after expanding synonyms - -- Always ignore coercions (not user written) -- ToDo: ignore invisible arguments? See Note [Invisible arguments and termination] instance Outputable PatersonSize where @@ -2422,21 +2432,26 @@ pSizeZero, pSizeOne :: PatersonSize pSizeZero = PS_Vanilla { ps_tvs = [], ps_size = 0 } pSizeOne = PS_Vanilla { ps_tvs = [], ps_size = 1 } -ltPatersonSize :: PatersonSize -- Size of constraint - -> PatersonSize -- Size of instance head; never PS_TyFam +-- | @ltPatersonSize ps1 ps2@ returns: +-- +-- - @Nothing@ iff @ps1@ is definitely strictly smaller than @ps2@, +-- - @Just ps_fail@ otherwise; @ps_fail@ says what went wrong. +ltPatersonSize :: PatersonSize + -> PatersonSize -> Maybe PatersonSizeFailure --- (ps1 `ltPatersonSize` ps2) returns --- Nothing iff ps1 is strictly smaller than p2 --- Just ps_fail says what went wrong -ltPatersonSize (PS_TyFam tc) _ = Just (PSF_TyFam tc) ltPatersonSize (PS_Vanilla { ps_tvs = tvs1, ps_size = s1 }) (PS_Vanilla { ps_tvs = tvs2, ps_size = s2 }) | s1 >= s2 = Just PSF_Size | bad_tvs@(_:_) <- noMoreTyVars tvs1 tvs2 = Just (PSF_TyVar bad_tvs) | otherwise = Nothing -- OK! -ltPatersonSize (PS_Vanilla {}) (PS_TyFam tc) - = pprPanic "ltPSize" (ppr tc) - -- Impossible because we never have a type family in an instance head +ltPatersonSize (PS_TyFam tc) _ = Just (PSF_TyFam tc) +ltPatersonSize _ (PS_TyFam tc) = Just (PSF_TyFam tc) + -- NB: this last equation is never taken when checking instances, because + -- type families are disallowed in instance heads. + -- + -- However, this function is also used in the logic for solving superclass + -- constraints (see Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance), + -- in which case we might well hit this case (see e.g. T23171). noMoreTyVars :: [TyVar] -- Free vars (with repetitions) of the constraint C -> [TyVar] -- Free vars (with repetitions) of the head H diff --git a/testsuite/tests/typecheck/should_compile/T23171.hs b/testsuite/tests/typecheck/should_compile/T23171.hs new file mode 100644 index 0000000000..93a217d0fe --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T23171.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module T23171 where + +import Data.Kind + +type C1 :: Type -> Type -> Constraint +class C1 t m where + +type C2 :: Type -> Constraint +class C2 a where + +type C3 :: Type -> Constraint +class C2 a => C3 a where + +type D :: Type -> Constraint +class D t where +instance (forall m. C3 m => C1 t m) => D t where + +type T :: Type -> Type +type family T a where + +try :: forall (e :: Type). D (T e) => e -> () +try _ = () + +type C1T :: Type -> Type -> Constraint +class C1 (T e) m => C1T e m + +tried :: forall (e :: Type). (forall m. C1T e m) => e -> () +tried = try @e + +-- From the call to "try", we get [W] D (T e). +-- After using the instance for D, we get the QC [G] C3 m ==> [W] C1 (T e) m. +-- +-- The Given "[G] C3 m" thus arises from superclass expansion +-- from "D (T e)", which contains a type family application, T. +-- So the logic in 'mkStrictSuperClasses' better be able to handle that when +-- expanding the superclasses of C3 (in this case, C2); in particular +-- ltPatersonSize needs to handle a type family in its second argument. + diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 4ffb6f6a5c..7ef8cc4fa6 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -871,5 +871,6 @@ test('T22194', normal, compile, ['']) test('QualifiedRecordUpdate', [ extra_files(['QualifiedRecordUpdate_aux.hs']) ] , multimod_compile, ['QualifiedRecordUpdate', '-v0']) +test('T23171', normal, compile, ['']) test('T23192', normal, compile, ['']) test('T23199', normal, compile, ['']) |