[Git][ghc/ghc][wip/T25647] Wibble

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Wed Feb 5 09:46:05 UTC 2025 


Simon Peyton Jones pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC


Commits:
5b1c26f7 by Simon Peyton Jones at 2025-02-05T09:45:50+00:00
Wibble

- - - - -


5 changed files:

- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- testsuite/tests/typecheck/should_compile/T25647_fail.hs
- + testsuite/tests/typecheck/should_compile/T25647_fail.stderr
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3360,24 +3360,52 @@ So, we use bindOuterFamEqnTKBndrs (which does not create an implication for
 the telescope), and generalise over /all/ the variables in the LHS,
 without treating the explicitly-quantified ones specially. Wrinkles:
 
- - When generalising, include the explicit user-specified forall'd
+(GT1) When generalising, include the explicit user-specified forall'd
    variables, so that we get an error from Validity.checkFamPatBinders
    if a forall'd variable is not bound on the LHS
 
- - We still want to complain about a bad telescope among the user-specified
+(GT2) We still want to complain about a bad telescope among the user-specified
    variables.  So in checkFamTelescope we emit an implication constraint
    quantifying only over them, purely so that we get a good telescope error.
 
-  - Note that, unlike a type signature like
+(GT3) Note that, unlike a type signature like
        f :: forall (a::k). blah
     we do /not/ care about the Inferred/Specified designation or order for
     the final quantified tyvars.  Type-family instances are not invoked
     directly in Haskell source code, so visible type application etc plays
     no role.
 
-See also Note [Re-quantify type variables in rules] in
-GHC.Tc.Gen.Rule, which explains a /very/ similar design when
-generalising over the type of a rewrite rule.
+(GT4) Consider #25647 (with UnliftedNewtypes)
+         type N :: forall r. (TYPE r -> TYPE r) -> TYPE r
+         newtype N f where { MkN :: ff (N ff) -> N ff }
+    When kind-checking the type signature for MkN we'll start wtih
+           ff :: TYPE kappa -> TYPE kappa
+           MkN :: ff (N @kappa) ff -> N @kappa ff
+    Then we generalise /and default the RuntimeRep variable kappa/
+    (via `kindGeneralizeAll` in `tcConDecl`), thus kappa := LiftedRep
+
+    But now the newtype looks like a GADT and we get an error
+         A newtype must not be a GADT
+
+    This seems OK.  We are just following the rules.
+
+    But this variant (the original report in #25647)
+       data family Fix2 :: (k -> Type) -> k
+       newtype instance Fix2 f where { In2 :: f (Fix2 f) -> Fix2 f }
+    At the `newtype instance`, we first
+       1. Find the kind of the newtype instance in `tcDataFamInstHeader`
+       2. Typecheck the newtype definitition itself in `tcConDecl`
+    In step 1 we do /not/ want to get
+       newtype instance forall r .  Fix2 (f :: TYPE r -> TYPE r) :: TYPE r where
+    If we do, we'll get that same "newtype must not be GADT" error as for N above.
+    Rather, we want to default the RuntimeRep variable r := LiftedRep. Hence
+    the use of `DefaultNonStandardTyVars` in `tcDataFamInstHeader`.  The key thing
+    is that we must make the /same/ choice here as we do in kind-checking the data
+    constructor's type.
+
+See also Note [Re-quantify type variables in rules] in GHC.Tc.Gen.Rule, which
+explains a /very/ similar design when generalising over the type of a rewrite
+rule.
 
 -}
 


=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -976,6 +976,9 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
        -- See GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
        ; dvs  <- candidateQTyVarsWithBinders outer_tvs lhs_ty
        ; qtvs <- quantifyTyVars skol_info DefaultNonStandardTyVars dvs
+                 -- DefaultNonStandardTyVars: see (GT4) in 
+                 -- GHC.Tc.TyCl Note [Generalising in tcTyFamInstEqnGuts]
+
        ; let final_tvs = scopedSort (qtvs ++ outer_tvs)
              -- This scopedSort is important: the qtvs may be /interleaved/ with
              -- the outer_tvs.  See Note [Generalising in tcTyFamInstEqnGuts]


=====================================
testsuite/tests/typecheck/should_compile/T25647_fail.hs
=====================================
@@ -5,54 +5,13 @@ module T25647 where
 import GHC.Exts
 import Data.Kind
 
--------------------- Plain newtypes -----------------
-
 -- Rejected because in the type signature for In2 we default
 -- the runtime-rep variable to LiftedRep, and that makes In2
 -- into a GADT
 newtype Fix2 f :: TYPE r where
    In2 :: forall ff. ff (Fix2 ff) -> Fix2 ff
 
--- Rejected because of defulting; maybe that's OK
+-- Rejected for the same reason
 type Fix4a :: forall r. (TYPE r -> TYPE r) -> TYPE r
 newtype Fix4a f where
   In4a :: ff (Fix4a ff) -> Fix4a ff
-
--- This variant produces a /terrible/ message
--- type Fix3a :: forall r k. (TYPE r -> TYPE r) -> TYPE r
--- newtype Fix3a f = In3a (f (Fix3 f))
-
--------------------- Data families with newtype instance -----------------
-
--- data instance in GADT sytntax
-data family Dix1 :: (k -> Type) -> k
-data instance Dix1 f where
-  DIn1 :: forall ff. ff (Dix1 ff) -> Dix1 ff
-
--- newtype instance in GADT syntax
-data family Dix2 :: (k -> Type) -> k
-newtype instance Dix2 f where
-  DIn2 :: forall ff. ff (Dix2 ff) -> Dix2 ff
-
-data family Dix2a :: (k -> Type) -> k
-newtype instance Dix2a f :: Type where
-  DIn2a :: forall ff. ff (Dix2a ff) -> Dix2a ff
-
--- newtype instance in H98 syntax
-data family Dix3 :: (k -> Type) -> k
-newtype instance Dix3 f = DIn3 (f (Dix3 f))
-
--- newtype instance in GADT syntax
--- Rejected because of defaulting
-data family Dix4 :: (k -> TYPE r) -> k
-newtype instance Dix4 f where
-  DIn4 :: forall ff. ff (Dix4 ff) -> Dix4 ff
-
-data family Dix4a :: (k -> TYPE r) -> k
-newtype instance forall r f. Dix4a f :: TYPE r where
-  DIn4a :: forall r (ff :: TYPE r -> TYPE r). ff (Dix4a ff) -> Dix4a ff
-
--- newtype instance in H98 syntax
-data family Dix5 :: (k -> TYPE r) -> k
-newtype instance Dix5 f = DIn5 (f (Dix5 f))
-


=====================================
testsuite/tests/typecheck/should_compile/T25647_fail.stderr
=====================================
@@ -0,0 +1 @@
+ 
\ No newline at end of file


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -933,4 +933,5 @@ test('T25266', normal, compile, [''])
 test('T25266a', normal, compile_fail, [''])
 test('T25266b', normal, compile, [''])
 test('T25597', normal, compile, [''])
-test('T25725', normal, compile, [''])
+test('T25647', normal, compile, [''])
+test('T25647_fail', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5b1c26f70045663c0c68bbacfb4f48259975dd1b

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5b1c26f70045663c0c68bbacfb4f48259975dd1b
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/20250205/c2a35b38/attachment-0001.html>

More information about the ghc-commits mailing list