[Git][ghc/ghc][wip/jakobbruenker/23515] Draft: Type/data instances: require that the instantiation is determined by the LHS alone (#23515)
Jakob Brünker (@JakobBruenker)
gitlab at gitlab.haskell.org
Tue May 28 02:23:54 UTC 2024
Jakob Brünker pushed to branch wip/jakobbruenker/23515 at Glasgow Haskell Compiler / GHC
Commits:
e28e6995 by Jakob Bruenker at 2024-05-28T04:23:16+02:00
Draft: Type/data instances: require that the instantiation is determined by the LHS alone (#23515)
- - - - -
23 changed files:
- compiler/GHC/Tc/TyCl.hs
- libraries/ghc-internal/src/GHC/Internal/Data/Type/Equality.hs
- testsuite/tests/dependent/should_compile/RaeJobTalk.hs
- testsuite/tests/dependent/should_compile/T14991.hs
- testsuite/tests/dependent/should_fail/T11471.hs
- testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.hs
- testsuite/tests/indexed-types/should_compile/GADT1.hs
- testsuite/tests/indexed-types/should_compile/GADT11.hs
- testsuite/tests/indexed-types/should_compile/Numerals.hs
- testsuite/tests/indexed-types/should_compile/T11715b.hs
- testsuite/tests/indexed-types/should_compile/T12522.hs
- testsuite/tests/indexed-types/should_compile/T13705.hs
- testsuite/tests/indexed-types/should_fail/T12041.hs
- testsuite/tests/indexed-types/should_fail/T13971.hs
- testsuite/tests/indexed-types/should_fail/T13971.stderr
- testsuite/tests/indexed-types/should_fail/T14246.hs
- testsuite/tests/indexed-types/should_fail/T14246.stderr
- testsuite/tests/patsyn/should_fail/T14507.hs
- testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
- testsuite/tests/polykinds/T11255.hs
- testsuite/tests/saks/should_compile/saks017.hs
- testsuite/tests/th/ClosedFam2TH.hs
- utils/haddock/html-test/src/TypeFamilies.hs
Changes:
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3330,7 +3330,7 @@ tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
-> HsOuterFamEqnTyVarBndrs GhcRn -- Implicit and explicit binders
-> HsFamEqnPats GhcRn -- Patterns
-> LHsType GhcRn -- RHS
- -> TcM ([TyVar], TyVarSet, [TcType], TcType)
+ -> TcM ([TyVar], TyVarSet, [Type], Type)
-- (tyvars, non_user_tvs, pats, rhs)
-- Used only for type families, not data families
tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
@@ -3342,15 +3342,14 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
-- This code is closely related to the code
-- in GHC.Tc.Gen.HsType.kcCheckDeclHeader_cusk
- ; (tclvl, wanted, (outer_bndrs, (lhs_ty, rhs_ty)))
+ ; (tclvl, wanted, (outer_bndrs, (lhs_ty, rhs_kind)))
<- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
bindOuterFamEqnTKBndrs skol_info outer_hs_bndrs $
do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
; addConsistencyConstraints mb_clsinfo lhs_ty
- ; rhs_ty <- tcCheckLHsTypeInContext hs_rhs_ty (TheKind rhs_kind)
- ; return (lhs_ty, rhs_ty) }
+ ; return (lhs_ty, rhs_kind) }
; outer_bndrs <- scopedSortOuter outer_bndrs
; let outer_tvs = outerTyVars outer_bndrs
@@ -3377,26 +3376,36 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
, text "lhs_ty:" <+> ppr lhs_ty
, text "final_tvs:" <+> pprTyVars final_tvs ]
- -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
- -- Example: typecheck/should_fail/T17301
- ; dvs_rhs <- candidateQTyVarsOfType rhs_ty
- ; let err_ctx tidy_env
- = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
- ; return (tidy_env2, UninfTyCtx_TyFamRhs rhs_ty) }
- ; doNotQuantifyTyVars dvs_rhs err_ctx
+ ; (tclvl_rhs, wanted_rhs, rhs_ty) <-
+ pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
+ tcExtendTyVarEnv final_tvs $
+ tcCheckLHsType hs_rhs_ty rhs_kind
+
+ ; reportUnsolvedEqualities skol_info final_tvs tclvl_rhs wanted_rhs
- ; (final_tvs, non_user_tvs, lhs_ty, rhs_ty) <- initZonkEnv NoFlexi $
+ ; (final_tvs, non_user_tvs, lhs_ty) <- initZonkEnv NoFlexi $
runZonkBndrT (zonkTyBndrsX final_tvs) $ \ final_tvs ->
do { lhs_ty <- zonkTcTypeToTypeX lhs_ty
- ; rhs_ty <- zonkTcTypeToTypeX rhs_ty
; non_user_tvs <- traverse lookupTyVarX qtvs
- ; return (final_tvs, non_user_tvs, lhs_ty, rhs_ty) }
+ ; return (final_tvs, non_user_tvs, lhs_ty) }
; let pats = unravelFamInstPats lhs_ty
-- Note that we do this after solveEqualities
-- so that any strange coercions inside lhs_ty
-- have been solved before we attempt to unravel it
+ -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+ -- Example: typecheck/should_fail/T17301
+ ; dvs_rhs <- candidateQTyVarsOfType rhs_kind
+ ; let err_ctx tidy_env
+ = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_kind
+ ; return (tidy_env2, UninfTyCtx_TyFamRhs rhs_ty) }
+ ; doNotQuantifyTyVars dvs_rhs err_ctx
+
+ ; rhs_ty <- initZonkEnv NoFlexi $
+ runZonkBndrT (zonkTyBndrsX final_tvs) $ \_ ->
+ zonkTcTypeToTypeX rhs_ty
+
; traceTc "tcTyFamInstEqnGuts }" (vcat [ ppr fam_tc, pprTyVars final_tvs ])
-- Don't try to print 'pats' here, because lhs_ty involves
-- a knot-tied type constructor, so we get a black hole
=====================================
libraries/ghc-internal/src/GHC/Internal/Data/Type/Equality.hs
=====================================
@@ -180,7 +180,7 @@ infix 4 ==
-- | A type family to compute Boolean equality.
type (==) :: k -> k -> Bool
type family a == b where
- f a == g b = f == g && a == b
+ f (a :: k) == g (b :: k) = f == g && a == b
a == a = 'True
_ == _ = 'False
=====================================
testsuite/tests/dependent/should_compile/RaeJobTalk.hs
=====================================
@@ -65,7 +65,7 @@ data Schema :: forall k. [k] -> Type where
Nil :: Schema '[]
(:>>) :: Sing h -> Schema t -> Schema (h ': t)
infixr 5 :>>
-type instance Sing = Schema
+type instance Sing @[k] = Schema
-- Append singleton lists
(%:++) :: Schema a -> Schema b -> Schema (a ++ b)
@@ -269,11 +269,11 @@ instance TestEquality TypeRep where
-- More singletons
-- a TypeRep really is a singleton
-type instance Sing = (TypeRep :: Type -> Type)
+type instance Sing @Type = (TypeRep :: Type -> Type)
data SSymbol :: Symbol -> Type where
SSym :: KnownSymbol s => SSymbol s
-type instance Sing = SSymbol
+type instance Sing @Symbol = SSymbol
instance TestEquality SSymbol where
testEquality :: forall s1 s2. SSymbol s1 -> SSymbol s2 -> Maybe (s1 :~: s2)
@@ -307,7 +307,7 @@ type Col = 'Attr
-- Singleton for columns
data SColumn :: Column -> Type where
Col :: Sing s -> TypeRep ty -> SColumn (Col s ty)
-type instance Sing = SColumn
+type instance Sing @Column = SColumn
-- Extract the type of a column
type family ColType col where
=====================================
testsuite/tests/dependent/should_compile/T14991.hs
=====================================
@@ -32,4 +32,4 @@ type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
-type instance Promote (a -> b) = PromoteX a ~> PromoteX b
+type instance Promote ((a :: Type) -> (b :: Type)) = PromoteX a ~> PromoteX b
=====================================
testsuite/tests/dependent/should_fail/T11471.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes #-}
+{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes, DataKinds #-}
module T11471 where
@@ -8,7 +8,7 @@ import Data.Kind
type family F a :: k
-type instance F Int = Int#
+type instance F @(TYPE IntRep) Int = Int#
f :: forall (a :: Type). Proxy a -> F a -> F a
-- NB: Those calls to F are (F @Type a)
=====================================
testsuite/tests/indexed-types/should_compile/ExplicitForAllFams2.hs
=====================================
@@ -31,9 +31,9 @@ instance forall a. Cl (Maybe a) where
-- Should produce warnings
type family N a where
- forall t a. N (t a) = [a]
- forall a. N a = ()
+ forall t (a :: Type). N (t a) = [a]
+ forall a. N a = ()
type family N' a where
- N' (t a) = [a]
- N' a = ()
+ N' (t (a :: Type)) = [a]
+ N' a = ()
=====================================
testsuite/tests/indexed-types/should_compile/GADT1.hs
=====================================
@@ -6,8 +6,10 @@
module GADT1 where
+import Data.Kind
+
data ZERO
-data SUCC n
+data SUCC (n :: Type)
data Nat n where
Zero :: Nat ZERO
=====================================
testsuite/tests/indexed-types/should_compile/GADT11.hs
=====================================
@@ -2,8 +2,10 @@
module ShouldCompile where
+import Data.Kind
+
data Z
-data S a
+data S (a :: Type)
type family Sum n m
type instance Sum n Z = n
=====================================
testsuite/tests/indexed-types/should_compile/Numerals.hs
=====================================
@@ -7,8 +7,8 @@ module Numerals where
import Data.Kind
-data Z -- empty data type
-data S a -- empty data type
+data Z -- empty data type
+data S (a :: Type) -- empty data type
data SNat n where -- natural numbers as singleton type
Zero :: SNat Z
=====================================
testsuite/tests/indexed-types/should_compile/T11715b.hs
=====================================
@@ -10,7 +10,7 @@ import Data.Kind ( Constraint )
type Id :: ( k -> Constraint ) -> l -> Constraint
type family Id a
-type instance Id f = f
+type instance Id @k @k f = f
type T = Id Eq (Eq Bool)
-- this should remain stuck, instead of
=====================================
testsuite/tests/indexed-types/should_compile/T12522.hs
=====================================
@@ -5,9 +5,11 @@
module T12522 where
+import Data.Kind (Type)
+
foo = f (Just 'c')
-data D1 x
+data D1 (x :: Type)
data D2
type family TF x = t | t -> x
=====================================
testsuite/tests/indexed-types/should_compile/T13705.hs
=====================================
@@ -3,7 +3,9 @@
module T13705 where
-data D x
+import Data.Kind (Type)
+
+data D (x :: Type)
type family F t = s | s -> t
type instance F (D t) = D (F t)
=====================================
testsuite/tests/indexed-types/should_fail/T12041.hs
=====================================
@@ -9,4 +9,4 @@ class Category (p :: i -> i -> Type) where
data I a b
instance Category I where
- type Ob I = (~) Int
+ type Ob @Type I = (~) Int
=====================================
testsuite/tests/indexed-types/should_fail/T13971.hs
=====================================
@@ -2,6 +2,8 @@
{-# LANGUAGE TypeFamilies #-}
module T13971 where
+import Data.Kind (Type)
+
class C a where
type T a :: k
- type T a = Int
+ type T @Type a = Int
=====================================
testsuite/tests/indexed-types/should_fail/T13971.stderr
=====================================
@@ -1,5 +1,5 @@
-T13971.hs:7:3: error: [GHC-41522]
+T13971.hs:9:3: error: [GHC-41522]
• Illegal argument ‘*’ in:
‘type T @{k} @(*) a = ...’
The arguments to ‘T’ must all be distinct type variables.
=====================================
testsuite/tests/indexed-types/should_fail/T14246.hs
=====================================
@@ -22,5 +22,5 @@ type family KLN n where
type Reveal :: forall k. forall (n :: k) -> Vect (KLN n) L -> Type
type family Reveal n l where
- Reveal (f :: v -> k) (Cons (Label (t :: v)) l) = Reveal (f t) l
+ Reveal (f :: v -> k) (Cons @Type @(KLN (f t)) (Label (t :: v)) l) = Reveal (f t) l
Reveal (a :: Type) Nil = a
=====================================
testsuite/tests/indexed-types/should_fail/T14246.stderr
=====================================
@@ -7,17 +7,10 @@ T14246.hs:20:5: error: [GHC-91510]
T14246.hs:25:27: error: [GHC-83865]
• Couldn't match kind ‘*’ with ‘L’
Expected kind ‘Vect (KLN f) L’,
- but ‘Cons (Label (t :: v)) l’ has kind ‘Vect (S (KLN (f t))) (*)’
+ but ‘Cons @Type @(KLN (f t)) (Label (t :: v)) l’ has kind ‘Vect
+ (S (KLN (f t))) (*)’
• In the second argument of ‘Reveal’, namely
- ‘(Cons (Label (t :: v)) l)’
- In the type family declaration for ‘Reveal’
-
-T14246.hs:25:67: error: [GHC-83865]
- • Couldn't match kind ‘*’ with ‘L’
- Expected kind ‘Vect (KLN (f t)) L’,
- but ‘l’ has kind ‘Vect (KLN (f t)) (*)’
- • In the second argument of ‘Reveal’, namely ‘l’
- In the type ‘Reveal (f t) l’
+ ‘(Cons @Type @(KLN (f t)) (Label (t :: v)) l)’
In the type family declaration for ‘Reveal’
T14246.hs:26:24: error: [GHC-83865]
=====================================
testsuite/tests/patsyn/should_fail/T14507.hs
=====================================
@@ -13,7 +13,7 @@ foo rep = error "urk"
type SING :: k -> Type
type family SING @k where
- SING = (TypeRep :: Bool -> Type)
+ SING @Bool = TypeRep
pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
=====================================
testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
=====================================
@@ -49,7 +49,7 @@ f5 = \case
-- f6 = \case
data Zero
-data Succ n
+data Succ (n :: Type)
type TenC n = Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ n)))))))))
=====================================
testsuite/tests/polykinds/T11255.hs
=====================================
@@ -3,4 +3,4 @@
module T11255 where
type family Default :: k
-type instance Default = '(Default, Default)
+type instance Default @(k1, k2) = '(Default, Default)
=====================================
testsuite/tests/saks/should_compile/saks017.hs
=====================================
@@ -7,7 +7,7 @@ import Data.Kind (Type)
type family F a where
F Bool = Type
- F (f a) = F a
+ F (f (a :: Type)) = F a
type family G a where
G Int = Type
=====================================
testsuite/tests/th/ClosedFam2TH.hs
=====================================
@@ -16,11 +16,11 @@ $( return [ KiSigD (mkName "Equals")
( TyVarSig (KindedTV (mkName "r") () (VarT (mkName "k"))))
Nothing)
[ TySynEqn Nothing
- (AppT (AppT (ConT (mkName "Equals")) (VarT (mkName "a")))
+ (AppT (AppT (AppKindT (ConT (mkName "Equals")) StarT) (VarT (mkName "a")))
(VarT (mkName "a")))
(ConT (mkName "Int"))
, TySynEqn Nothing
- (AppT (AppT (ConT (mkName "Equals")) (VarT (mkName "a")))
+ (AppT (AppT (AppKindT (ConT (mkName "Equals")) StarT) (VarT (mkName "a")))
(VarT (mkName "b")))
(ConT (mkName "Bool")) ] ])
=====================================
utils/haddock/html-test/src/TypeFamilies.hs
=====================================
@@ -32,9 +32,9 @@ instance Test Y
type family Foo a :: k
-- | Doc for: type instance Foo X = Y
-type instance Foo X = Y
+type instance Foo @Type X = Y
-- | Doc for: type instance Foo Y = X
-type instance Foo Y = X
+type instance Foo @Type Y = X
-- | Doc for: data family Bat a
data family Bat (a :: k) :: Type
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e28e69955b43c6a6caf9eaece31e47b73cc396e1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e28e69955b43c6a6caf9eaece31e47b73cc396e1
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/20240527/61ad845f/attachment-0001.html>
More information about the ghc-commits
mailing list