[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