[GHC] #15471: Polymorphism, typed splices and type inference don't mix

[GHC]

#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