diff options
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 33 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_compile/T11635.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_compile/T11719.hs | 18 | ||||
| -rw-r--r-- | 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 552c0d05b4..2b226f267b 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 0000000000..1cbdbafb90 --- /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 0000000000..ba4d7c9db4 --- /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 2f9d311f4f..5985fd9fbb 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, ['']) |