[commit: ghc] master: Fix #11635 / #11719. (1701255)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/1701255c06fed2aa2811f7f29f108d88fc4d6f26/ghc

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

commit 1701255c06fed2aa2811f7f29f108d88fc4d6f26
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Fri Mar 18 11:02:38 2016 -0400

    Fix #11635 / #11719.
    
    Instead of creating a new meta-tyvar and then unifying it with
    a known kind in a KindedTyVar in a LHsQTyVars, just use the known kind.
    
    Sadly, this still doesn't make #11719 usable, because while you can
    now define a higher-kinded type family, you can't write any equations
    for it, which is a larger problem.
    
    test cases: dependent/should_compile/T{11635,11719}


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

1701255c06fed2aa2811f7f29f108d88fc4d6f26
 compiler/typecheck/TcHsType.hs                     | 33 +++++++++++-----------
 testsuite/tests/dependent/should_compile/T11635.hs |  7 +++++
 testsuite/tests/dependent/should_compile/T11719.hs | 18 ++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  2 ++
 4 files changed, 44 insertions(+), 16 deletions(-)

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 552c0d0..2b226f2 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -83,7 +83,7 @@ import PrelNames hiding ( wildCardName )
 import Pair
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.Maybe
+import Maybes
 import Data.List ( partition )
 import Control.Monad
 
@@ -1291,7 +1291,7 @@ kcHsTyVarBndrs cusk open_fam all_kind_vars
 
     kc_hs_tv :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
     kc_hs_tv (UserTyVar (L _ name))
-      = do { tv_pair@(tv, scoped) <- tcHsTyVarName name
+      = do { tv_pair@(tv, scoped) <- tcHsTyVarName Nothing name
 
               -- Open type/data families default their variables to kind *.
            ; when (open_fam && not scoped) $ -- (don't default class tyvars)
@@ -1301,13 +1301,8 @@ kcHsTyVarBndrs cusk open_fam all_kind_vars
            ; return tv_pair }
 
     kc_hs_tv (KindedTyVar (L _ name) lhs_kind)
-      = do { tv_pair@(tv, _) <- tcHsTyVarName name
-           ; kind <- tcLHsKind lhs_kind
-               -- for a scoped variable: make sure annotation is consistent
-               -- for an unscoped variable: unify the meta-tyvar kind
-               -- either way: we can ignore the resulting coercion
-           ; discardResult $ unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
-           ; return tv_pair }
+      = do { kind <- tcLHsKind lhs_kind
+           ; tcHsTyVarName (Just kind) name }
 
     report_non_cusk_tvs all_tvs
       = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
@@ -1330,7 +1325,7 @@ tcImplicitTKBndrs :: [Name]
                   -> TcM (a, TyVarSet)   -- vars are bound somewhere in the scope
                                          -- see Note [Scope-check inferred kinds]
                   -> TcM ([TcTyVar], a)
-tcImplicitTKBndrs = tcImplicitTKBndrsX tcHsTyVarName
+tcImplicitTKBndrs = tcImplicitTKBndrsX (tcHsTyVarName Nothing)
 
 -- | Convenient specialization
 tcImplicitTKBndrsType :: [Name]
@@ -1414,16 +1409,22 @@ tcHsTyVarBndr (KindedTyVar (L _ name) kind)
   = do { kind <- tcLHsKind kind
        ; return (mkTcTyVar name kind (SkolemTv False)) }
 
--- | Produce a tyvar of the given name (with a meta-tyvar kind). If
--- the name is already in scope, return the scoped variable. The
+-- | Produce a tyvar of the given name (with the kind provided, or
+-- otherwise a meta-var kind). If
+-- the name is already in scope, return the scoped variable, checking
+-- to make sure the known kind matches any kind provided. The
 -- second return value says whether the variable is in scope (True)
 -- or not (False). (Use this for associated types, for example.)
-tcHsTyVarName :: Name -> TcM (TcTyVar, Bool)
-tcHsTyVarName name
+tcHsTyVarName :: Maybe Kind -> Name -> TcM (TcTyVar, Bool)
+tcHsTyVarName m_kind name
   = do { mb_tv <- tcLookupLcl_maybe name
        ; case mb_tv of
-           Just (ATyVar _ tv) -> return (tv, True)
-           _ -> do { kind <- newMetaKindVar
+           Just (ATyVar _ tv)
+             -> do { whenIsJust m_kind $ \ kind ->
+                     discardResult $
+                     unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
+                   ; return (tv, True) }
+           _ -> do { kind <- maybe newMetaKindVar return m_kind
                    ; return (mkTcTyVar name kind vanillaSkolemTv, False) }}
 
 -- makes a new skolem tv
diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs
new file mode 100644
index 0000000..1cbdbaf
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T11635.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
+
+module T11635 where
+
+import Data.Kind
+
+data X (a :: forall k. k -> * ) b = X
diff --git a/testsuite/tests/dependent/should_compile/T11719.hs b/testsuite/tests/dependent/should_compile/T11719.hs
new file mode 100644
index 0000000..ba4d7c9
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T11719.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE RankNTypes, TypeFamilies, TypeInType, TypeOperators,
+             UndecidableInstances #-}
+
+module T11719 where
+
+import Data.Kind
+
+data TyFun :: * -> * -> *
+type a ~> b = TyFun a b -> *
+
+type family (f :: a ~> b) @@ (x :: a) :: b
+
+data Null a = Nullable a | NotNullable a
+
+type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
+  (f ∘ g) x = f @@ (g @@ x)
+
+type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where   -- this fails :(
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 2f9d311..5985fd9 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -19,3 +19,5 @@ test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
 test('T11711', normal, compile, [''])
 test('RaeJobTalk', normal, compile, [''])
+test('T11635', normal, compile, [''])
+test('T11719', normal, compile, [''])