[GHC] #14279: Type families interfere with specialisation rewrite rules
#14279: Type families interfere with specialisation rewrite rules -------------------------------------+------------------------------------- Reporter: IvanTimokhin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the attached file, in particular the function {{{#!hs vinr :: Length as -> VSum bs -> VSum (as ++ bs) }}} its specialised version {{{#!hs vinr0 :: Length '[] -> VSum as -> VSum as }}} and the rewrite rule {{{#!hs {-# RULES "vinr/0" vinr = vinr0 #-} }}} According to [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... the relevant section of GHC user guide], `vinr` should be replaced with `vinr0` whenever the types match. However, the resulting Core for `test` contains the following (compiled with `ghc -O2`): {{{#!hs Test.test1 = case extractIdx @ 'Z @ '[Int] @ Int (Test.$WIZ @ Int @ '[]) Test.test2 of { Left other_aZf -> Test.$wvinl @ Length @ '[Int] @ (Remove 'Z '[Int]) other_aZf; Right x_aZg -> vinr @ (Remove 'Z '[Int]) @ '[Int] (Test.$WLZ `cast` ((Length (Sym (Test.D:R:Remove[0] <Int>_N <'[]>_N)))_R :: (Length '[] :: *) ~R# (Length (Remove 'Z '[Int]) :: *))) (Test.VInL @ '[Int] @ Int @ '[] @~ (<'[Int]>_N :: ('[Int] :: [*]) GHC.Prim.~# ('[Int] :: [*])) x_aZg) } }}} So the rule never fires, and `vinr` is still there, even though it is directly applied to `LZ :: Length '[]`. My dilettante analysis is that, for some reason, GHC keeps the `Remove 'Z '[Int]` as-is, not evaluating it to `'[]`, and, since the types don't match //syntactically//, doesn't apply the rule. In particular, if I replace type families with classes with functional dependencies, the rule fires as expected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14279 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14279: Type families interfere with specialisation rewrite rules -------------------------------------+------------------------------------- Reporter: IvanTimokhin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by IvanTimokhin): * Attachment "test.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14279 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14279: Type families interfere with specialisation rewrite rules -------------------------------------+------------------------------------- Reporter: IvanTimokhin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14279#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14279: Type families interfere with specialisation rewrite rules
-------------------------------------+-------------------------------------
Reporter: IvanTimokhin | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.1
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Other | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
Your analysis is right. We have something like
{{{
test = replace @ 'Z
@ '[Int]
@ '[Int]
@ Int
(Test.$WLZ
`cast` ((Length (Sym (Test.D:R:Remove[0] <Int>_N
<'[]>_N)))_R
:: (Length '[] :: *) ~R# (Length (Remove 'Z
'[Int]) :: *)))
(Test.$WLS @ '[] @ Int Test.$WLZ)
(Test.$WIZ @ Int @ '[])
(Test.$WVInL @ Int @ '[])
(Test.$WVInL @ Int @ '[] (GHC.Types.I# 2#)))
}}}
where the RHS of `replace` has various occurrences of `Remove n as`. If
we inline `replace`
for this call site, those occurrences become `Remove 'Z '[Int]`, which
you'd like to
see reduced to `'[]`. But the rule matcher does not match modulo
function reduction.
Perhaps it should. But it't not clear to me how. Suppose we have an axiom
{{{
ax :: F Int ~ Bool
}}}
and we have a call
{{{
...(f @(Maybe (F Int)) e1 e2)...
}}}
Perhaps, before (or somehow during) the matching of a rule for `f`, we
should
transform to
{{{
...(f @(Maybe Bool) e1 e2)...
}}}
But that isn't well typed; we'd need to do some `liftCoSubst` kind of
thing. Suppose
{{{
f :: forall a. ty<a>
and
co :: s1 ~ s2 -- s2 is a normalised version of s1
}}}
Then perhaps we can rewrite
{{{
f @s1
===>
f @s2 |> ty[sym co/a]
}}}
Perhaps something like this (maybe a bit more; e.g. on binder types)
can replace the handful of
uses of `topNormaliseType_maybe` in the simplifier. Or, more generally,
perhaps we can do this normalisation in `simplType`. It would make sense
for the simplifier to aggressively normalise types, as inlining happens,
just
as it normalises terms.
Why do fundeps work? I think it's because the function appliation does
not
appear nested inside `replace`, but rather is passed as an argument to
`replace`,
and hence can be normalised in the caller.
I wonder if other people have tripped over this lack of normalisation
in types in the simplifier?
I don't think this would be hard to try out.
--
Ticket URL:
#14279: Type families interfere with specialisation rewrite rules -------------------------------------+------------------------------------- Reporter: IvanTimokhin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I argue that (related to my musings in #14119), patterns -- such as that LHS of rules -- should not mention type families at all. In other words, we should change any `F ty` in rule LHS to a fresh type variable `a` and then require `F ty ~ a`. Which, as it turns out, is precisely what's done in my [http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf Constrained Type Families] paper. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14279#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14279: Type families interfere with specialisation rewrite rules
-------------------------------------+-------------------------------------
Reporter: IvanTimokhin | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.1
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Other | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
But the LHS of the rule does ''not'' mention a type family, so comment:3
is irrelevant to this particular ticket. Here is the rule:
{{{
==================== Tidy Core rules ====================
"vinr/0"
forall (@ (as :: [*])).
vinr @ '[] @ as
= (vinr0 @ as)
`cast` (
#14279: Type families interfere with specialisation rewrite rules -------------------------------------+------------------------------------- Reporter: IvanTimokhin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Ah yes. The unreduced type family is in the ''target'', not the rule. I was skimming too quickly. In agreement with comment:2, I argue this is very much like my new `flatten_args` (see Phab:D3848). GHC's flattener is a component of its constraint solver that essentially implements a strongly-typed rewrite system, where the equations of the rewrite system are 1) type family equations, 2) assumed equalities (e.g., from GADTs), and 3) filled-in metavariables. Of course, a RULE is just an equation to be used in a rewrite system, just the same. The problem is that the two rewrite system implementations are utterly distinct within GHC, where it seems like they should be combined somehow. And, following on from comment:2, the new logic in my Phab:D3848 patch would need to be applied here, too. Interesting. I think this is doable, but I don't think it's done lightly (unlike Simon's conclusion above). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14279#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC