diff options
Diffstat (limited to 'testsuite/tests/dependent/should_compile')
6 files changed, 123 insertions, 1 deletions
diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs new file mode 100644 index 0000000000..47957d47d6 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/InferDependency.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE TypeInType #-} + +module InferDependency where + +data Proxy k (a :: k) +data Proxy2 k a = P (Proxy k a) diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs index 1cbdbafb90..2292def966 100644 --- a/testsuite/tests/dependent/should_compile/T11635.hs +++ b/testsuite/tests/dependent/should_compile/T11635.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-} +{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-} module T11635 where diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs new file mode 100644 index 0000000000..e1a6255520 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14066a.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs, + UndecidableInstances, RankNTypes, ScopedTypeVariables #-} + +module T14066a where + +import Data.Proxy +import Data.Kind +import Data.Type.Bool + + +type family Bar x y where + Bar (x :: a) (y :: b) = Int + Bar (x :: c) (y :: d) = Bool -- a,b,c,d should be SigTvs and unify appropriately + + + -- the two k's, even though they have different scopes, should unify in the + -- kind-check and then work in the type-check because Prox3 has been generalized + +data Prox3 a where + MkProx3a :: Prox3 (a :: k1) + MkProx3b :: Prox3 (a :: k2) + + -- This probably should be rejected, as it's polymorphic recursion without a CUSK. + -- But GHC accepts it because the polymorphic occurrence is at a type variable. +data T0 a = forall k (b :: k). MkT0 (T0 b) Int + + -- k and j should unify +type family G x a where + G Int (b :: k) = Int + G Bool (c :: j) = Bool + +-- this last example just checks that GADT pattern-matching on kinds still works. +-- nothing new here. +data T (a :: k) where + MkT :: T (a :: Type -> Type) + +data S (a :: Type -> Type) where + MkS :: S a + +f :: forall k (a :: k). Proxy a -> T a -> () +f _ MkT = let y :: S a + y = MkS + in () + +-- This is questionable. Should we use the RHS to determine dependency? It works +-- now, but if it stops working in the future, that's not a deal-breaker. +type P k a = Proxy (a :: k) + + +-- This is a challenge. It should be accepted, but only because c's kind is learned +-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind, +-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`. +-- Naively, we don't know about c's kind early enough. + +data SameKind :: forall k. k -> k -> Type +type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where + IfK (_ :: Proxy True) f _ = f + IfK (_ :: Proxy False) _ g = g +x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True)) +x _ = Proxy + + +f2 :: forall b. b -> Proxy Maybe +f2 x = fstOf3 y :: Proxy Maybe + where + y :: (Proxy a, Proxy c, b) + y = (Proxy, Proxy, x) + +fstOf3 (x, _, _) = x + +f3 :: forall b. b -> Proxy Maybe +f3 x = fst y :: Proxy Maybe + where + y :: (Proxy a, b) + y = (Proxy, x) + +-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables, +-- so it is generalized, even with MonoLocalBinds. +f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe) + where + y :: (Proxy a, Int) + y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr new file mode 100644 index 0000000000..906695f3f7 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14066a.stderr @@ -0,0 +1,5 @@ + +T14066a.hs:13:3: warning: + Type family instance equation is overlapped: + forall c d (x :: c) (y :: d). + Bar x y = Bool -- Defined at T14066a.hs:13:3 diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs new file mode 100644 index 0000000000..79bcce66ff --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14749.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-} + +module T14749 where + +import Data.Kind + +data KIND = STAR | KIND :> KIND + +data Ty :: KIND -> Type where + TMaybe :: Ty (STAR :> STAR) + TApp :: Ty (a :> b) -> (Ty a -> Ty b) + +type family IK (k :: KIND) = (res :: Type) where + IK STAR = Type + IK (a:>b) = IK a -> IK b + +type family I (t :: Ty k) = (res :: IK k) where + I TMaybe = Maybe + I (TApp f a) = (I f) (I a) + +data TyRep (k :: KIND) (t :: Ty k) where + TyMaybe :: TyRep (STAR:>STAR) TMaybe + TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x) + +zero :: TyRep STAR a -> I a +zero x = case x of + TyApp TyMaybe _ -> Nothing diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index da25b22799..070e1203f8 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -32,3 +32,5 @@ test('T13938', [extra_files(['T13938a.hs'])], run_command, ['$MAKE -s --no-print-directory T13938']) test('T14556', normal, compile, ['']) test('T14720', normal, compile, ['']) +test('T14066a', normal, compile, ['']) +test('T14749', normal, compile, ['']) |