#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * failure: None/Unknown => GHC rejects valid program * component: Compiler => Template Haskell -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Well, we have {{{ teset_foo :: forall p. Q (TExp (p -> p)) }}} When we run a top-level splice, as in `$$(test_foo)`, we're going to run it at compile time; it's like running it in GHCi; it must be a closed expression. So GHC must pick a type to instantiate `p`; and it chooses `Any`. After all, `test_foo` could also have type {{{ test_foo :: forall p. Num p => p -> Q (TExp (p -> p)) }}} and now we must pick a `Num` dictionary to pass to it. I think what you want is for `test_foo` to have type {{{ test_foo :: Q (TExp (forall p. p->p)) }}} but we can't do that. Yet anyway. For a start it'd require impredicative polymorphism. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm only saying "it's behaving as specified". (So not a bug in that sense.) I think you want to propose an extension to the existing behaviour. What is that extension? Specifically, what type do you expect `test_foo` to have? I don't know what this has to do with static forms, but from your `foo` I get {{{ • No instance for (Typeable a0) arising from a static form • In the expression: static (id :: forall a. a -> a) In an equation for ‘foo’: foo = static (id :: forall a. a -> a) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Replying to [comment:6 simonpj]:

I'm only saying "it's behaving as specified". (So not a bug in that sense.)

I think you want to propose an extension to the existing behaviour. What is that extension? Specifically, what type do you expect `test_foo` to have?

I don't know what this has to do with static forms, but from your `foo` I get {{{ • No instance for (Typeable a0) arising from a static form • In the expression: static (id :: forall a. a -> a) In an equation for ‘foo’: foo = static (id :: forall a. a -> a) }}}

I think that the type of the quote is fine but problem is during the type checking of typed splices. The fact that the metaocaml example works also supports this I think. The relevance of the static form example is that the type of `static id` should surely follow the same logic as the type of `[|| id ||]`. The inferred type of `static id` is `foo :: forall a . (Typeable a, IsStatic t) => t (a -> a)`. It is then very surprising when the dereferencing/splicing behaviour differs between the cases. {{{ {-# LANGUAGE StaticPointers #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TemplateHaskell #-} module SP where foo = static id foo2 = [|| id ||] }}} So I don't have a concrete suggestion to what exactly goes wrong but I suspect that the typed splice typechecking code is somehow suspect. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): `test_foo` should have type `forall a . Q (TExp (a -> a))`. Which is the same as in metaocaml. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): The inferred type of `test_foo2` is exactly what you suggest it shouldn't be unless I am misunderstaning. {{{ *SP> :t test_foo2 test_foo2 :: forall {a}. Num a => Language.Haskell.TH.Syntax.Q (Language.Haskell.TH.Syntax.TExp (a -> a)) }}} The difference is now that you can't splice back in `test_foo2` without instantiating `a` as otherwise the ambiguous type variable stops `Num a` being solved. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): After chatting with Matthew at ICFP, we identified that the really troubling thing about this ticket is the inconsistency between the typing of `qux` with (works) and without (fails) a type signature. This is mentioned in the Description, but I had not focused on it before. On investigation, I find it is worse than I thought. Consider {{{ {-# LANGUAGE TemplateHaskell #-} module Def where import Language.Haskell.TH foo :: Q (TExp a) -> Q (TExp [a]) foo x = [|| [ $$x, $$x ] ||] }}} This defines a perfectly decent typed-TH function `foo`. Now try {{{ {-# LANGUAGE TemplateHaskell #-} module Foo where import Language.Haskell.TH import TH bar y = $$(foo [|| y ||] ) }}} Note, no type signature. What type gets inferred for `bar`? Answer {{{ TYPE SIGNATURES bar :: GHC.Types.Any -> [GHC.Types.Any] }}} Yikes! Of course it should be {{{ bar :: a -> [a] }}} and indeed that type signature works. Why does this happen? Becuase `TcSplice.tcTopSplice` calls `tcTopSpliceExpr`, and the latter concludes with {{{ -- Zonk it and tie the knot of dictionary bindings ; zonkTopLExpr (mkHsDictLet (EvBinds const_binds) expr') } }}} At this moment the type checker is inside `bar`'s `\y -> ...`, so we have `y :: alpha` for some as-yet-unknown unification variable `alpha`. Alas, the `zonkTopLExpr` turns that unification variable into `Any`, and after that there is no way back. One way out might be to make the zonker less aggressive; make it leave unification variables alone. But that means that the entire optimisation pipeline would, for the first time, have to accommodate unification variables in Core terms. Currently it's an invariant that no such unification variables exist. I don't think anything would actually break, but it Just Seems Wrong. Richard suggested an interesting alternative: defer actually ''running'' typed-TH splices until the zonker, or the desugarer. When we encounter `$$( e )` we have to: 1. Typecheck `e`, ensuring it has type `Q (TExp ty)`; then `$$( e )` has type `ty`. 2. Compile and run the code `e`, to generate some (renamed) `HsSyn` code. 3. Typecheck the `HsSyn GhcRn` code it generates, to add the elaboration: type abstractions type applications and so on. Because it's ''typed'' TH, we know that (3) can't fail. So at typecheck time we could do (1) and stop, leaving steps (2) and (3) to be done after typechecking is complete. Interesting. There's a real bug here. I like the idea of deferring running the splice. I'm not sure whether the desugarer or the zonker is best. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5286 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * differential: => Phab:D5286 Comment: I attempted a patch: https://phabricator.haskell.org/D5286 I will add a note once it's confirmed that this is the right approach but it correctly deals with the examples in the ticket. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: fixed | Keywords: | TypedTemplateHaskell Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: th/T15471 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5286, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/106 -------------------------------------+------------------------------------- Changes (by mpickering): * keywords: => TypedTemplateHaskell -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15471: Polymorphism, typed splices and type inference don't mix -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.4.3 Resolution: fixed | Keywords: | TypedTemplateHaskell Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: th/T15471 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5286, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/106 -------------------------------------+------------------------------------- Comment (by Marge Bot <ben+marge-bot@…>): In [changeset:"a48753bdbc99cda36890e851950f5b79e1c3b2b2/ghc" a48753b/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="a48753bdbc99cda36890e851950f5b79e1c3b2b2" Capture and simplify constraints arising from running typed splices This fixes a regression caused by #15471 where splicing in a trivial program such as `[|| return () ||]` would fail as the dictionary for `return` would never get bound in the module containing the splice. Arguably this is symptomatic of a major problem affecting TTH where we serialise renamed asts and then retype check them. The reference to the dictionary should be fully determined at the quote site so that splicing doesn't have to solve any implicits at all. It's a coincidence this works due to coherence but see #15863 and #15865 for examples where things do go very wrong. Fixes #16195 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15471#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler