summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/typecheck/TcCanonical.hs40
-rw-r--r--compiler/types/Coercion.hs3
-rw-r--r--testsuite/tests/indexed-types/should_fail/T2544.stderr12
-rw-r--r--testsuite/tests/polykinds/T14172.stderr15
-rw-r--r--testsuite/tests/typecheck/should_compile/T16188.hs48
-rw-r--r--testsuite/tests/typecheck/should_compile/T16204a.hs58
-rw-r--r--testsuite/tests/typecheck/should_compile/T16204b.hs58
-rw-r--r--testsuite/tests/typecheck/should_compile/T16225.hs25
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T4
-rw-r--r--testsuite/tests/typecheck/should_fail/T16204c.hs16
-rw-r--r--testsuite/tests/typecheck/should_fail/T16204c.stderr12
-rw-r--r--testsuite/tests/typecheck/should_fail/all.T1
12 files changed, 251 insertions, 41 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index a1451a83bc..d643925127 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1576,11 +1576,15 @@ canDecomposableTyConAppOK :: CtEvidence -> EqRel
-> TcS ()
-- Precondition: tys1 and tys2 are the same length, hence "OK"
canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
- = case ev of
+ = ASSERT( tys1 `equalLength` tys2 )
+ case ev of
CtDerived {}
-> unifyDeriveds loc tc_roles tys1 tys2
CtWanted { ctev_dest = dest }
+ -- new_locs and tc_roles are both infinite, so
+ -- we are guaranteed that cos has the same length
+ -- as tys1 and tys2
-> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
; setWantedEq dest (mkTyConAppCo role tc cos) }
@@ -1596,21 +1600,29 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
where
loc = ctEvLoc ev
role = eqRelRole eq_rel
- tc_roles = tyConRolesX role tc
-
- -- the following makes a better distinction between "kind" and "type"
- -- in error messages
- bndrs = tyConBinders tc
- is_kinds = map isNamedTyConBinder bndrs
- is_viss = map isVisibleTyConBinder bndrs
- kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
- vis_xforms = map (\is_vis -> if is_vis then id
- else flip updateCtLocOrigin toInvisibleOrigin)
- is_viss
+ -- infinite, as tyConRolesX returns an infinite tail of Nominal
+ tc_roles = tyConRolesX role tc
- -- zipWith3 (.) composes its first two arguments and applies it to the third
- new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
+ -- Add nuances to the location during decomposition:
+ -- * if the argument is a kind argument, remember this, so that error
+ -- messages say "kind", not "type". This is determined based on whether
+ -- the corresponding tyConBinder is named (that is, dependent)
+ -- * if the argument is invisible, note this as well, again by
+ -- looking at the corresponding binder
+ -- For oversaturated tycons, we need the (repeat loc) tail, which doesn't
+ -- do either of these changes. (Forgetting to do so led to #16188)
+ --
+ -- NB: infinite in length
+ new_locs = [ new_loc
+ | bndr <- tyConBinders tc
+ , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
+ | otherwise = loc
+ new_loc | isVisibleTyConBinder bndr
+ = updateCtLocOrigin new_loc0 toInvisibleOrigin
+ | otherwise
+ = new_loc0 ]
+ ++ repeat loc
-- | Call when canonicalizing an equality fails, but if the equality is
-- representational, there is some hope for the future.
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 701c674aaf..7bb85740ac 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1317,10 +1317,13 @@ applyRoles tc cos
-- the Role parameter is the Role of the TyConAppCo
-- defined here because this is intimately concerned with the implementation
-- of TyConAppCo
+-- Always returns an infinite list (with a infinite tail of Nominal)
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Representational tc = tyConRolesRepresentational tc
tyConRolesX role _ = repeat role
+-- Returns the roles of the parameters of a tycon, with an infinite tail
+-- of Nominal
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 93d7746066..6b1a6bd075 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,16 +1,4 @@
-T2544.hs:19:12: error:
- • Couldn't match type ‘IxMap r’ with ‘IxMap i1’
- Expected type: IxMap (l :|: r) [Int]
- Actual type: BiApp (IxMap l) (IxMap i1) [Int]
- NB: ‘IxMap’ is a non-injective type family
- The type variable ‘i1’ is ambiguous
- • In the expression: BiApp empty empty
- In an equation for ‘empty’: empty = BiApp empty empty
- In the instance declaration for ‘Ix (l :|: r)’
- • Relevant bindings include
- empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
-
T2544.hs:19:18: error:
• Couldn't match type ‘IxMap i0’ with ‘IxMap l’
Expected type: IxMap l [Int]
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index f85cf66d79..41790105cb 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -24,18 +24,3 @@ T14172.hs:7:19: error:
• Relevant bindings include
traverseCompose :: (a -> f b) -> g a -> f (h a')
(bound at T14172.hs:7:1)
-
-T14172.hs:7:19: error:
- • Couldn't match type ‘g’ with ‘Compose f'0 g'1’
- ‘g’ is a rigid type variable bound by
- the inferred type of
- traverseCompose :: (a -> f b) -> g a -> f (h a')
- at T14172.hs:7:1-46
- Expected type: (a -> f b) -> g a -> f (h a')
- Actual type: (a -> f b) -> Compose f'0 g'1 a -> f (h a')
- • In the expression: _Wrapping Compose . traverse
- In an equation for ‘traverseCompose’:
- traverseCompose = _Wrapping Compose . traverse
- • Relevant bindings include
- traverseCompose :: (a -> f b) -> g a -> f (h a')
- (bound at T14172.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_compile/T16188.hs b/testsuite/tests/typecheck/should_compile/T16188.hs
new file mode 100644
index 0000000000..31144198a3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16188.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T16188 where
+
+import Data.Kind (Type)
+import Data.Type.Bool (type (&&))
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+data family Sing :: forall k. k -> Type
+
+data instance Sing :: Bool -> Type where
+ SFalse :: Sing False
+ STrue :: Sing True
+
+(%&&) :: forall (x :: Bool) (y :: Bool).
+ Sing x -> Sing y -> Sing (x && y)
+SFalse %&& _ = SFalse
+STrue %&& a = a
+
+data RegExp :: Type -> Type where
+ App :: RegExp t -> RegExp t -> RegExp t
+
+data instance Sing :: forall t. RegExp t -> Type where
+ SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
+
+data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
+type instance Apply ReNotEmptySym0 r = ReNotEmpty r
+
+type family ReNotEmpty (r :: RegExp t) :: Bool where
+ ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
+
+sReNotEmpty :: forall t (r :: RegExp t).
+ Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
+sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
+
+blah :: forall (t :: Type) (re :: RegExp t).
+ Sing re -> ()
+blah (SApp sre1 sre2)
+ = case (sReNotEmpty sre1, sReNotEmpty sre2) of
+ (STrue, STrue) -> ()
diff --git a/testsuite/tests/typecheck/should_compile/T16204a.hs b/testsuite/tests/typecheck/should_compile/T16204a.hs
new file mode 100644
index 0000000000..63cae41d8c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16204a.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204 where
+
+import Data.Kind
+
+-----
+-- singletons machinery
+-----
+
+data family Sing :: forall k. k -> Type
+data SomeSing :: Type -> Type where
+ SomeSing :: Sing (a :: k) -> SomeSing k
+
+-----
+-- (Simplified) GHC.Generics
+-----
+
+class Generic (a :: Type) where
+ type Rep a :: Type
+ from :: a -> Rep a
+ to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+ -- type PFrom ...
+ type PTo (x :: Rep a) :: a
+
+class SGeneric k where
+ -- sFrom :: ...
+ sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+-----
+
+class SingKind k where
+ type Demote k :: Type
+ -- fromSing :: ...
+ toSing :: Demote k -> SomeSing k
+
+genericToSing :: forall k.
+ ( SingKind k, SGeneric k, SingKind (Rep k)
+ , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
+ => Demote k -> SomeSing k
+genericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo
+
+withSomeSing :: forall k r
+ . SingKind k
+ => Demote k
+ -> (forall (a :: k). Sing a -> r)
+ -> r
+withSomeSing x f =
+ case toSing x of
+ SomeSing x' -> f x'
diff --git a/testsuite/tests/typecheck/should_compile/T16204b.hs b/testsuite/tests/typecheck/should_compile/T16204b.hs
new file mode 100644
index 0000000000..12f7391f49
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16204b.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204b where
+
+import Data.Kind
+
+-----
+-- singletons machinery
+-----
+
+data family Sing :: forall k. k -> Type
+data SomeSing :: Type -> Type where
+ SomeSing :: Sing (a :: k) -> SomeSing k
+
+-----
+-- (Simplified) GHC.Generics
+-----
+
+class Generic (a :: Type) where
+ type Rep a :: Type
+ from :: a -> Rep a
+ to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+ -- type PFrom ...
+ type PTo (x :: Rep a) :: a
+
+class SGeneric k where
+ -- sFrom :: ...
+ sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+-----
+
+class SingKind k where
+ type Demote k :: Type
+ -- fromSing :: ...
+ toSing :: Demote k -> SomeSing k
+
+genericToSing :: forall k.
+ ( SingKind k, SGeneric k, SingKind (Rep k)
+ , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
+ => Demote k -> SomeSing k
+genericToSing d = withSomeSing (from d) $ SomeSing . sTo
+
+withSomeSing :: forall k r
+ . SingKind k
+ => Demote k
+ -> (forall (a :: k). Sing a -> r)
+ -> r
+withSomeSing x f =
+ case toSing x of
+ SomeSing x' -> f x'
diff --git a/testsuite/tests/typecheck/should_compile/T16225.hs b/testsuite/tests/typecheck/should_compile/T16225.hs
new file mode 100644
index 0000000000..85c5441327
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16225.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T16225 where
+
+import Data.Kind
+
+data family Sing :: k -> Type
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+
+data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
+type instance Apply (TyCon1 f) x = f x
+
+data SomeApply :: (k ~> Type) -> Type where
+ SomeApply :: Apply f a -> SomeApply f
+
+f :: SomeApply (TyCon1 Sing :: k ~> Type)
+ -> SomeApply (TyCon1 Sing :: k ~> Type)
+f (SomeApply s)
+ = SomeApply s
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3ee0a9f6d4..dae5b6feea 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -665,3 +665,7 @@ test('T16033', normal, compile, [''])
test('T16141', normal, compile, ['-O'])
test('T15549a', normal, compile, [''])
test('T15549b', normal, compile, [''])
+test('T16188', normal, compile, [''])
+test('T16204a', normal, compile, [''])
+test('T16204b', normal, compile, [''])
+test('T16225', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.hs b/testsuite/tests/typecheck/should_fail/T16204c.hs
new file mode 100644
index 0000000000..97318a5729
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16204c.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204c where
+
+import Data.Kind
+
+data family Sing :: forall k. k -> Type
+type family Rep :: Type
+
+sTo :: forall (a :: Rep). Sing a
+sTo = sTo
+
+x :: forall (a :: Type). Sing a
+x = id sTo
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.stderr b/testsuite/tests/typecheck/should_fail/T16204c.stderr
new file mode 100644
index 0000000000..48d63785ad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16204c.stderr
@@ -0,0 +1,12 @@
+
+T16204c.hs:16:8: error:
+ • Couldn't match kind ‘Rep’ with ‘*’
+ When matching types
+ a0 :: Rep
+ a :: *
+ Expected type: Sing a
+ Actual type: Sing a0
+ • In the first argument of ‘id’, namely ‘sTo’
+ In the expression: id sTo
+ In an equation for ‘x’: x = id sTo
+ • Relevant bindings include x :: Sing a (bound at T16204c.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 52f02cfcf5..3f7e820d05 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -510,3 +510,4 @@ test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail,
test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
['T16059e', '-v0'])
test('T16255', normal, compile_fail, [''])
+test('T16204c', normal, compile_fail, [''])
View Lorry Controller Status