[commit: ghc] wip/T15809: More progress with data instances (0849475)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T15809
Link       : http://ghc.haskell.org/trac/ghc/changeset/084947591fc538e67d8e40211685a5cb2ff6b575/ghc

>---------------------------------------------------------------

commit 084947591fc538e67d8e40211685a5cb2ff6b575
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Nov 14 15:25:45 2018 +0000

    More progress with data instances
    
    Slightly controversially, I adjusted T15725 to have
    
      data Sing :: k -> *
    
    rather than
    
      data Sing :: forall k. k -> *
    
    See a fc-call thread.  We could revisit this if need be;
    it's not fundamental to the line of progress.


>---------------------------------------------------------------

084947591fc538e67d8e40211685a5cb2ff6b575
 compiler/typecheck/TcDeriv.hs                      |  2 +-
 compiler/typecheck/TcInstDcls.hs                   |  1 -
 compiler/typecheck/TcTyClsDecls.hs                 | 17 +++++++++++------
 testsuite/tests/dependent/should_compile/T15725.hs |  6 +++---
 testsuite/tests/ghci/scripts/T10059.stdout         |  6 +++---
 testsuite/tests/ghci/scripts/ghci059.stdout        |  2 +-
 6 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index bb9c76b..147191b 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -786,7 +786,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
            -- we want to drop type variables from T so that (C d (T a)) is well-kinded
           let (arg_kinds, _)  = splitFunTys cls_arg_kind
               n_args_to_drop  = length arg_kinds
-              n_args_to_keep  = tyConArity tc - n_args_to_drop
+              n_args_to_keep  = length tc_args - n_args_to_drop
               (tc_args_to_keep, args_to_drop)
                               = splitAt n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 86ed84a..d1081a2 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -738,7 +738,6 @@ tcDataFamInstDecl mb_clsinfo
          -- Kind check type patterns
        ; let exp_bndrs = mb_bndrs `orElse` []
              data_ctxt = DataKindCtxt (unLoc fam_name)
-       ; 
 
        ; (_, (_, (pats, stupid_theta, res_kind)))
                <- pushTcLevelM_                                $
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index c8a182a..4de2238 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1485,17 +1485,22 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
 
-  -- Check the kind signature, if any.
-  -- Data families might have a variable return kind.
-  -- See See Note [Arity of data families] in FamInstEnv.
-  ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
+  -- Check that the result kind is OK
+  -- We allow things like
+  --   data family T (a :: Type) :: forall k. k -> Type
+  -- We treat T as having arity 1, but result kind forall k. k -> Type
+  -- But we want to check that the result kind finishes in
+  --   Type or a kind-variable
+  -- For the latter, consider
+  --   data family D a :: forall k. Type -> k
+  ; let (_, final_res_kind) = splitPiTys res_kind
   ; checkTc (tcIsLiftedTypeKind final_res_kind
              || isJust (tcGetCastedTyVar_maybe final_res_kind))
             (badKindSig False res_kind)
 
   ; tc_rep_name <- newTyConRepName tc_name
-  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
-                              final_res_kind
+  ; let tycon = mkFamilyTyCon tc_name binders
+                              res_kind
                               (resultVariableName sig)
                               (DataFamilyTyCon tc_rep_name)
                               parent NotInjective
diff --git a/testsuite/tests/dependent/should_compile/T15725.hs b/testsuite/tests/dependent/should_compile/T15725.hs
index a5f259e..1e2e171 100644
--- a/testsuite/tests/dependent/should_compile/T15725.hs
+++ b/testsuite/tests/dependent/should_compile/T15725.hs
@@ -23,12 +23,12 @@ instance SC Identity
 
 -------------------------------------------------------------------------------
 
-data family Sing :: forall k. k -> Type
-data instance Sing :: forall a. Identity a -> Type where
+data family Sing :: k -> Type
+data instance Sing ::  Identity a -> Type where
   SIdentity :: Sing x -> Sing ('Identity x)
 
 newtype Par1 p = Par1 p
-data instance Sing :: forall p. Par1 p -> Type where
+data instance Sing ::  Par1 p -> Type where
   SPar1 :: Sing x -> Sing ('Par1 x)
 
 type family Rep1 (f :: Type -> Type) :: Type -> Type
diff --git a/testsuite/tests/ghci/scripts/T10059.stdout b/testsuite/tests/ghci/scripts/T10059.stdout
index 92fbb45..955c95a 100644
--- a/testsuite/tests/ghci/scripts/T10059.stdout
+++ b/testsuite/tests/ghci/scripts/T10059.stdout
@@ -1,4 +1,4 @@
-class (a ~ b) => (~) (a :: k0) (b :: k0) 	-- Defined in ‘GHC.Types’
-(~) :: k0 -> k0 -> Constraint
-class (a GHC.Prim.~# b) => (~) (a :: k0) (b :: k0)
+class (a ~ b) => (~) (a :: k) (b :: k) 	-- Defined in ‘GHC.Types’
+(~) :: k -> k -> Constraint
+class (a GHC.Prim.~# b) => (~) (a :: k) (b :: k)
   	-- Defined in ‘GHC.Types’
diff --git a/testsuite/tests/ghci/scripts/ghci059.stdout b/testsuite/tests/ghci/scripts/ghci059.stdout
index 9e9adb9..7e734f1 100644
--- a/testsuite/tests/ghci/scripts/ghci059.stdout
+++ b/testsuite/tests/ghci/scripts/ghci059.stdout
@@ -4,6 +4,6 @@ It is not a class.
 Please see section 9.14.4 of the user's guide for details.
 -}
 type role Coercible representational representational
-class Coercible a b => Coercible (a :: k0) (b :: k0)
+class Coercible a b => Coercible (a :: k) (b :: k)
   	-- Defined in ‘GHC.Types’
 coerce :: Coercible a b => a -> b 	-- Defined in ‘GHC.Prim’