Commit 4a4ae70f authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Fix #16188

There was an awful lot of zipping going on in
canDecomposableTyConAppOK, and one of the lists being zipped
was too short, causing the result to be too short. Easily
fixed.

Also fixes #16204 and #16225

test case: typecheck/should_compile/T16188
           typecheck/should_compile/T16204[ab]
           typecheck/should_fail/T16204c
           typecheck/should_compile/T16225
parent 012257c1
Pipeline #2124 passed with stages
in 475 minutes and 18 seconds
......@@ -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.
......
......@@ -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
......
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]
......
......@@ -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)
{-# 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) -> ()
{-# 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'
{-# 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'
{-# 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
......@@ -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, [''])
{-# 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
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)
......@@ -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, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment