[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: Lint: more details on "Occurrence is GlobalId, but binding is LocalId"

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Fri Jun 16 07:22:38 UTC 2023



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
c24c0e7d by Ben Price at 2023-06-16T03:22:28-04:00
Lint: more details on "Occurrence is GlobalId, but binding is LocalId"

This is helpful when debugging a pass which accidentally shadowed a
binder.

- - - - -
f7e3ca7a by Ryan Hendrickson at 2023-06-16T03:22:31-04:00
Clean a stray bit of text in user guide

- - - - -
047b8d26 by Vladislav Zavialov at 2023-06-16T03:22:32-04:00
testsuite: Add forall visibility test cases

The added tests ensure that the type checker does not confuse
visible and invisible foralls.

VisFlag1:    kind-checking type applications and inferred type variable instantiations
VisFlag1_ql: kind-checking Quick Look instantiations
VisFlag2:    kind-checking type family instances
VisFlag3:    checking kind annotations on type parameters of associated type families
VisFlag4:    checking kind annotations on type parameters in type declarations with SAKS
VisFlag5:    checking the result kind annotation of data family instances

- - - - -


15 changed files:

- compiler/GHC/Core/Lint.hs
- docs/users_guide/exts/infix_tycons.rst
- + testsuite/tests/typecheck/should_fail/VisFlag1.hs
- + testsuite/tests/typecheck/should_fail/VisFlag1.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs
- + testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag2.hs
- + testsuite/tests/typecheck/should_fail/VisFlag2.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag3.hs
- + testsuite/tests/typecheck/should_fail/VisFlag3.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag4.hs
- + testsuite/tests/typecheck/should_fail/VisFlag4.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag5.hs
- + testsuite/tests/typecheck/should_fail/VisFlag5.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -3243,7 +3243,7 @@ lookupIdInScope id_occ
   = do { in_scope_ids <- getInScopeIds
        ; case lookupVarEnv in_scope_ids id_occ of
            Just (id_bndr, linted_ty)
-             -> do { checkL (not (bad_global id_bndr)) global_in_scope
+             -> do { checkL (not (bad_global id_bndr)) $ global_in_scope id_bndr
                    ; return (id_bndr, linted_ty) }
            Nothing -> do { checkL (not is_local) local_out_of_scope
                          ; return (id_occ, idType id_occ) } }
@@ -3252,8 +3252,10 @@ lookupIdInScope id_occ
   where
     is_local = mustHaveLocalBinding id_occ
     local_out_of_scope = text "Out of scope:" <+> pprBndr LetBind id_occ
-    global_in_scope    = hang (text "Occurrence is GlobalId, but binding is LocalId")
-                            2 (pprBndr LetBind id_occ)
+    global_in_scope id_bndr = hang (text "Occurrence is GlobalId, but binding is LocalId")
+                                 2 $ vcat [hang (text "occurrence:") 2 $ pprBndr LetBind id_occ
+                                          ,hang (text "binder    :") 2 $ pprBndr LetBind id_bndr
+                                          ]
     bad_global id_bnd = isGlobalId id_occ
                      && isLocalId id_bnd
                      && not (isWiredIn id_occ)


=====================================
docs/users_guide/exts/infix_tycons.rst
=====================================
@@ -41,7 +41,7 @@ specifically:
          infixl 7 T, :*:
 
    sets the fixity for both type constructor ``T`` and data constructor
-   ``T``, and similarly for ``:*:``. ``Int `a` Bool``.
+   ``T``, and similarly for ``:*:``.
 
 -  The function arrow ``->`` is ``infixr`` with fixity -1.
 


=====================================
testsuite/tests/typecheck/should_fail/VisFlag1.hs
=====================================
@@ -0,0 +1,18 @@
+module VisFlag1 where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV


=====================================
testsuite/tests/typecheck/should_fail/VisFlag1.stderr
=====================================
@@ -0,0 +1,27 @@
+
+VisFlag1.hs:12:16: error: [GHC-83865]
+    • Expecting one more argument to ‘V’
+      Expected kind ‘forall j. j -> *’,
+        but ‘V’ has kind ‘forall k -> k -> *’
+    • In the type ‘V’
+      In the expression: f @V MkV
+      In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+VisFlag1.hs:15:15: error: [GHC-91028]
+    • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall j. j -> *
+    • In the expression: f @_ MkV
+      In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+VisFlag1.hs:18:15: error: [GHC-18872]
+    • Couldn't match kind: forall k -> k -> *
+                     with: forall j. j -> *
+      When matching types
+        hk0 :: forall j. j -> *
+        V :: forall k -> k -> *
+      Expected: hk0 a0
+        Actual: V k1 a0
+    • In the first argument of ‘f’, namely ‘MkV’
+      In the expression: f MkV
+      In an equation for ‘bad_infer’: bad_infer = f MkV


=====================================
testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs
=====================================
@@ -0,0 +1,20 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module VisFlag1_ql where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV


=====================================
testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
=====================================
@@ -0,0 +1,23 @@
+
+VisFlag1_ql.hs:14:16: error: [GHC-83865]
+    • Expecting one more argument to ‘V’
+      Expected kind ‘forall j. j -> *’,
+        but ‘V’ has kind ‘forall k -> k -> *’
+    • In the type ‘V’
+      In the expression: f @V MkV
+      In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+VisFlag1_ql.hs:17:15: error: [GHC-91028]
+    • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall j. j -> *
+    • In the expression: f @_ MkV
+      In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+VisFlag1_ql.hs:20:15: error: [GHC-83865]
+    • Expecting one more argument to ‘V’
+      Expected kind ‘forall j. j -> *’,
+        but ‘V’ has kind ‘forall k -> k -> *’
+    • In the first argument of ‘f’, namely ‘MkV’
+      In the expression: f MkV
+      In an equation for ‘bad_infer’: bad_infer = f MkV


=====================================
testsuite/tests/typecheck/should_fail/VisFlag2.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module VisFlag2 where
+
+import Data.Kind (Type)
+
+-- the (Type ->) parameter is to prevent instantiation of invisible variables
+
+type family Invis :: Type -> forall a.   a
+type family Vis   :: Type -> forall a -> a
+
+type instance Vis = Invis  -- Bad
+type instance Invis = Vis  -- Bad


=====================================
testsuite/tests/typecheck/should_fail/VisFlag2.stderr
=====================================
@@ -0,0 +1,15 @@
+
+VisFlag2.hs:13:21: error: [GHC-83865]
+    • Couldn't match kind: forall a. a
+                     with: forall a -> a
+      Expected kind ‘* -> forall a -> a’,
+        but ‘Invis’ has kind ‘* -> forall a. a’
+    • In the type ‘Invis’
+      In the type instance declaration for ‘Vis’
+
+VisFlag2.hs:14:23: error: [GHC-83865]
+    • Expecting one more argument to ‘Vis’
+      Expected kind ‘* -> forall a. a’,
+        but ‘Vis’ has kind ‘* -> forall a -> a’
+    • In the type ‘Vis’
+      In the type instance declaration for ‘Invis’


=====================================
testsuite/tests/typecheck/should_fail/VisFlag3.hs
=====================================
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module VisFlag3 where
+
+class C (hk :: forall k. k -> k) where
+  type F (hk :: forall k -> k -> k)


=====================================
testsuite/tests/typecheck/should_fail/VisFlag3.stderr
=====================================
@@ -0,0 +1,6 @@
+
+VisFlag3.hs:6:3: error: [GHC-83865]
+    • Expecting one more argument to ‘hk’
+      Expected kind ‘forall k. k -> k’,
+        but ‘hk’ has kind ‘forall k -> k -> k’
+    • In the associated type family declaration for ‘F’


=====================================
testsuite/tests/typecheck/should_fail/VisFlag4.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module VisFlag4 where
+
+import Data.Kind
+
+type C :: (forall k -> k -> k) -> Constraint
+class C (hk :: forall k. k -> k) where


=====================================
testsuite/tests/typecheck/should_fail/VisFlag4.stderr
=====================================
@@ -0,0 +1,5 @@
+
+VisFlag4.hs:8:1: error: [GHC-83865]
+    • Expected kind ‘forall k -> k -> k’,
+        but ‘hk’ has kind ‘forall k. k -> k’
+    • In the class declaration for ‘C’


=====================================
testsuite/tests/typecheck/should_fail/VisFlag5.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module VisFlag5 where
+
+import Data.Kind
+
+data family   D a   :: (forall i -> i -> i) -> Type
+data instance D Int :: (forall i.   i -> i) -> Type


=====================================
testsuite/tests/typecheck/should_fail/VisFlag5.stderr
=====================================
@@ -0,0 +1,7 @@
+
+VisFlag5.hs:8:1: error: [GHC-83865]
+    • Couldn't match kind: forall i -> i -> i
+                     with: forall i. i -> i
+      Expected kind ‘(forall i. i -> i) -> *’,
+        but ‘D Int’ has kind ‘(forall i -> i -> i) -> *’
+    • In the data instance declaration for ‘D’


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -690,3 +690,9 @@ test('T22560_fail_b', normal, compile_fail, [''])
 test('T22560_fail_c', normal, compile_fail, [''])
 test('T22560_fail_d', normal, compile_fail, [''])
 test('T22560_fail_ext', normal, compile_fail, [''])
+test('VisFlag1', normal, compile_fail, [''])
+test('VisFlag1_ql', normal, compile_fail, [''])
+test('VisFlag2', normal, compile_fail, [''])
+test('VisFlag3', normal, compile_fail, [''])
+test('VisFlag4', normal, compile_fail, [''])
+test('VisFlag5', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/efe7b16e80b9dca099809e34a508bad920dfea84...047b8d26e5b9039042ecc8fb0a21ea828a9cedc1

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/efe7b16e80b9dca099809e34a508bad920dfea84...047b8d26e5b9039042ecc8fb0a21ea828a9cedc1
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/20230616/e4142828/attachment-0001.html>


More information about the ghc-commits mailing list