[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: <http://ghc.haskell.org/trac/ghc/ticket/14279#comment:2> 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 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` (<Length '[]>_R ->_R <VSum as>_R ->_R (VSum (Sym (D:R:++[0] <as>_N)))_R :: Coercible (Length '[] -> VSum as -> VSum as) (Length '[] -> VSum as -> VSum ('[] ++ as))) }}} The trouble is that type family appears in the term we are matching the rule against. And it appears in the form `Remove 'Z '[Int]`. We can reduce that to `'[]`, which matches the rule. But we don't: hence my suggestions in comment:2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14279#comment:4> 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 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