[Git][ghc/ghc][wip/top-level-kind-signatures] Fix T16723 T16724: arity and instantiation

Vladislav Zavialov gitlab at gitlab.haskell.org
Fri May 31 19:39:40 UTC 2019



Vladislav Zavialov pushed to branch wip/top-level-kind-signatures at Glasgow Haskell Compiler / GHC


Commits:
d0c418f6 by Vladislav Zavialov at 2019-05-31T19:39:06Z
Fix T16723 T16724: arity and instantiation

- - - - -


6 changed files:

- compiler/typecheck/TcTyClsDecls.hs
- + testsuite/tests/tlks/should_compile/T16723.hs
- + testsuite/tests/tlks/should_compile/T16724.hs
- + testsuite/tests/tlks/should_compile/T16724.script
- testsuite/tests/tlks/should_compile/all.T
- testsuite/tests/tlks/should_compile/tlks025.script


Changes:

=====================================
compiler/typecheck/TcTyClsDecls.hs
=====================================
@@ -1245,18 +1245,23 @@ kcDeclHeader name arityGuard flav ki ktvs kc_res_ki =
        -> [(Name,TcTyVar)]      -- accumulated scoped type variables, reversed
        -> [LHsTyVarBndr GhcRn]  -- the header binders
        -> TcM TcTyCon
-    go d_ki subst tcb_acc stv_acc bndrs@(b:bs) =
+    go d_ki subst tcb_acc stv_acc bndrs =
       case tcSplitPiTy_maybe d_ki of
         Just (Named (Bndr v' argFlag at Specified), d_ki') ->
-          do { let b_ki = substTy subst (varType v')
-                   b_name = tyVarName v'
-             ; tcv <- newSkolemTyVar b_name b_ki
-             ; let tcb = mkNamedTyConBinder argFlag tcv
-                   stv = (b_name, tcv)
-                   subst' = extendTvSubst subst v' (mkTyVarTy tcv)
-             ; tcExtendNameTyVarEnv [stv] $
-               go d_ki' subst' (tcb:tcb_acc) (stv:stv_acc) bndrs
-             }
+          case bndrs of
+            [] | KeepPoly keep_n <- arityGuard,
+                 keep_n > 0
+               -> goSpecified1 keep_n d_ki subst tcb_acc stv_acc
+            _  ->
+              do { let b_ki = substTy subst (varType v')
+                       b_name = tyVarName v'
+                 ; tcv <- newSkolemTyVar b_name b_ki
+                 ; let tcb = mkNamedTyConBinder argFlag tcv
+                       stv = (b_name, tcv)
+                       subst' = extendTvSubst subst v' (mkTyVarTy tcv)
+                 ; tcExtendNameTyVarEnv [stv] $
+                   go d_ki' subst' (tcb:tcb_acc) (stv:stv_acc) bndrs
+                 }
         Just (Named (Bndr v' argFlag at Inferred), d_ki') ->
           do { let b_ki = substTy subst (varType v')
                    b_name = tyVarName v'
@@ -1273,32 +1278,39 @@ kcDeclHeader name arityGuard flav ki ktvs kc_res_ki =
              ; let tcb = mkAnonTyConBinder argFlag tcv
              ; go d_ki' subst (tcb:tcb_acc) stv_acc bndrs }
         Just (Anon argFlag at VisArg bndr_ki, d_ki') ->
-          do { let b_ki = substTy subst bndr_ki
-             ; v_name <- checkVar b_ki b
-             ; tcv <- newSkolemTyVar v_name b_ki
-             ; let tcb = mkAnonTyConBinder argFlag tcv
-                   stv = (v_name, tcv)
-             ; tcExtendNameTyVarEnv [stv] $
-               go d_ki' subst (tcb:tcb_acc) (stv:stv_acc) bs
-             }
+          case bndrs of
+            [] -> done (substTy subst d_ki) tcb_acc stv_acc
+            b:bs ->
+              do { let b_ki = substTy subst bndr_ki
+                 ; v_name <- checkVar b_ki b
+                 ; tcv <- newSkolemTyVar v_name b_ki
+                 ; let tcb = mkAnonTyConBinder argFlag tcv
+                       stv = (v_name, tcv)
+                 ; tcExtendNameTyVarEnv [stv] $
+                   go d_ki' subst (tcb:tcb_acc) (stv:stv_acc) bs
+                 }
         Just (Named (Bndr v' argFlag at Required), d_ki') ->
-          do { let b_ki = substTy subst (varType v')
-                   b_name = tyVarName v'
-             ; v_name <- checkVar b_ki b
-             ; tcv <- newSkolemTyVar b_name b_ki
-             ; let tcb = mkNamedTyConBinder argFlag tcv
-                   stv = (v_name, tcv)
-                   subst' = extendTvSubst subst v' (mkTyVarTy tcv)
-             ; tcExtendNameTyVarEnv [stv] $
-               go d_ki' subst' (tcb:tcb_acc) (stv:stv_acc) bs
-             }
-        Nothing -> failWithTc (tooManyBindersErr d_ki bndrs)
-    go d_ki subst tcb_acc stv_acc [] =
+          case bndrs of
+            [] -> done (substTy subst d_ki) tcb_acc stv_acc
+            b:bs ->
+              do { let b_ki = substTy subst (varType v')
+                       b_name = tyVarName v'
+                 ; v_name <- checkVar b_ki b
+                 ; tcv <- newSkolemTyVar b_name b_ki
+                 ; let tcb = mkNamedTyConBinder argFlag tcv
+                       stv = (v_name, tcv)
+                       subst' = extendTvSubst subst v' (mkTyVarTy tcv)
+                 ; tcExtendNameTyVarEnv [stv] $
+                   go d_ki' subst' (tcb:tcb_acc) (stv:stv_acc) bs
+                 }
+        Nothing ->
+          case bndrs of
+            [] -> done (substTy subst d_ki) tcb_acc stv_acc
+            _:_ -> failWithTc (tooManyBindersErr d_ki bndrs)
+
+    goSpecified1 keep_n d_ki subst tcb_acc stv_acc =
       do { let (specified, d_ki') = tcSplitForAllTysExactVis Specified d_ki
-               specified_n = length specified
-               can_inst = case arityGuard of
-                            InstAll -> specified_n
-                            KeepPoly keep_n -> max 0 (specified_n - keep_n)
+               can_inst = max 0 (length specified - keep_n)
          ; traceTc "kcDeclHeader specified =" (ppr specified)
          ; traceTc "kcDeclHeader can_inst =" (ppr can_inst)
          ; goSpecified can_inst specified d_ki' subst tcb_acc stv_acc


=====================================
testsuite/tests/tlks/should_compile/T16723.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE TopLevelKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T16723 where
+
+import Data.Kind
+
+type D :: forall a. Type
+data D


=====================================
testsuite/tests/tlks/should_compile/T16724.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE TopLevelKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T16724 where
+
+import Data.Kind
+
+type T1 :: forall k (a :: k). Type
+type family T1
+
+-- type T2 :: forall {k} (a :: k). Type
+type T2 :: forall a. Type
+type family T2


=====================================
testsuite/tests/tlks/should_compile/T16724.script
=====================================
@@ -0,0 +1,5 @@
+:set -fprint-explicit-kinds -fprint-explicit-foralls -XNoStarIsType
+:load T16724.hs
+:info T1
+:info T2
+   -- must have the same arity!


=====================================
testsuite/tests/tlks/should_compile/all.T
=====================================
@@ -29,3 +29,5 @@ test('tlks026', normal, compile, [''])
 test('tlks027', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('tlks028', normal, compile, [''])
 test('tlks029', normal, compile, [''])
+test('T16723', normal, compile, [''])
+test('T16724', extra_files(['T16724.hs']), ghci_script, ['T16724.script'])


=====================================
testsuite/tests/tlks/should_compile/tlks025.script
=====================================
@@ -1,3 +1,3 @@
-:set -XTopLevelKindSignatures -XTypeFamilies -XNoStarIsType
+:set -XNoStarIsType
 :load tlks025.hs
 :kind T



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/d0c418f63a06721a576b693a1dc3730c36439a0b

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/d0c418f63a06721a576b693a1dc3730c36439a0b
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/20190531/853a5737/attachment-0001.html>


More information about the ghc-commits mailing list