#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