[GHC] #10271: Typed Template Haskell splice difficulty when resolving overloading

[GHC]

#10271: Typed Template Haskell splice difficulty when resolving overloading
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.10.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> J Garrett Morris describes the following surprising
> behaviour for typed Template Haskell
> {{{
> {-# LANGUAGE TemplateHaskell, FlexibleInstances #-}
> module PrintfLib where
>     import Language.Haskell.TH
>
>     class Printf t where
>       printf :: String -> Q (TExp String) -> Q (TExp t)
>
>     instance Printf [Char] where
>       tf s t | '%' `notElem` s = [|| $$t ++ s ||]
>              | otherwise       = fail ("Unexpected format %"
>                                        ++ [c])
>       where (_, _:c:_) = break ('%' ==) s
>
>     instance Printf t => Printf (Char -> t) where
>       printf s t
>         | c /= 'c' = fail ("Unexpected format %" ++ [c] ++
>                            " for character")
>         | otherwise = [|| \c -> $$(printf s''
>                                      [|| $$t ++ s' ++ [c] ||])
>                        ||]
>           where (s', '%':c:s'') = break ('%' ==) s
>
> -------------------------
> {-# LANGUAGE TemplateHaskell #-}
> module Printf where
>     import PrintfLib
>
>     f :: Char -> String
>     f = $$(printf "foo %c" [||""||])
>
>     h :: Char -> String
>     h y = $$(printf "foo %c" [||""||]) y
> }}}
> Oddly, `f` typechecks but `h` does not, even though `h` is just an eta-
> expanded version of `f`:
> {{{
> Printf.hs:9:10:
>     No instance for (Printf t0) arising from a use of ‘printf’
>     The type variable ‘t0’ is ambiguous
>     Note: there are several potential instances:
>       instance Printf t => Printf (Char -> t) -- Defined in ‘PrintfLib’
>       instance Printf [Char] -- Defined in ‘PrintfLib’
>     In the expression: printf "foo %c" [|| "" ||]
> }}}
> What is going on?  Here's the deal
>
>  * To run the splice, GHC must solve any constraints that arise form the
> expression `(printf "foo %c" ...)`.
>  * Since `printf` is overloaded, and overloaded on its result type, the
> type needed by the context of the splice is what determines which
> instance of `Printf` is needed.
>  * In `f` the context needs `Char -> String`, and so the call to `printf`
> must have type `TExpr (Char -> String)`, so we get the constraint `Printf
> (Char -> String)` which we can solve.
>  * But in `h` the rule for application tries to ''infer'' a type for the
> splice.  So the context for the call just says `TExp t0` for some
> unification variable `t0`; and that leads to the insoluble constraint.
>
> You may say that GHC should be cleverer, and push that type signature
> information into the application. And perhaps it should.  But you can
> never win. For example:
> {{{
>   hard x = [ $$(printf "gluk" [|| "" ||]), undefined :: Char -> String ]
> }}}
> Here the RHS of `hard` is a 2-element list. Since all elements of a list
> have the same type,
> the splice must have the same type as the second element of the list,
> namely `Char->String`.  But seeing that would mean that we'd have to
> typecheck right-to-left.  In general GHC tries very very hard NOT to
> depend on traveral order.  There is no way in general to ensure that we
> have all the information now that constraint solving may ultimately
> produce.
>
> I'm not sure what to do about this.
>  * It seldom matters, because resolving the overloading on the splice
> seldom depends on the result type.
>  * When it does matter, you can fix it by giving a type signature to the
> splice itself.
> But it seems unsatisfactory.  Ideas welcome.

New description:

 J Garrett Morris describes the following surprising behaviour for typed
 Template Haskell
 {{{
 {-# LANGUAGE TemplateHaskell, FlexibleInstances #-}
 module PrintfLib where
     import Language.Haskell.TH

     class Printf t where
       printf :: String -> Q (TExp String) -> Q (TExp t)

     instance Printf [Char] where
       tf s t | '%' `notElem` s = [|| $$t ++ s ||]
              | otherwise       = fail ("Unexpected format %"
                                        ++ [c])
       where (_, _:c:_) = break ('%' ==) s

     instance Printf t => Printf (Char -> t) where
       printf s t
         | c /= 'c' = fail ("Unexpected format %" ++ [c] ++
                            " for character")
         | otherwise = [|| \c -> $$(printf s''
                                      [|| $$t ++ s' ++ [c] ||])
                        ||]
           where (s', '%':c:s'') = break ('%' ==) s

 -------------------------
 {-# LANGUAGE TemplateHaskell #-}
 module Printf where
     import PrintfLib

     f :: Char -> String
     f = $$(printf "foo %c" [||""||])

     h :: Char -> String
     h y = $$(printf "foo %c" [||""||]) y
 }}}
 Oddly, `f` typechecks but `h` does not, even though `h` is just an eta-
 expanded version of `f`:
 {{{
 Printf.hs:9:10:
     No instance for (Printf t0) arising from a use of ‘printf’
     The type variable ‘t0’ is ambiguous
     Note: there are several potential instances:
       instance Printf t => Printf (Char -> t) -- Defined in ‘PrintfLib’
       instance Printf [Char] -- Defined in ‘PrintfLib’
     In the expression: printf "foo %c" [|| "" ||]
 }}}
 What is going on?  Here's the deal

  * To run the splice, GHC must solve any constraints that arise form the
 expression `(printf "foo %c" ...)`.
  * Since `printf` is overloaded, and overloaded on its result type, the
 type needed by the context of the splice is what determines which instance
 of `Printf` is needed.
  * In `f` the context needs `Char -> String`, and so the call to `printf`
 must have type `TExpr (Char -> String)`, so we get the constraint `Printf
 (Char -> String)` which we can solve.
  * But in `h` the rule for application tries to ''infer'' a type for the
 splice.  So the context for the call just says `TExp t0` for some
 unification variable `t0`; and that leads to the insoluble constraint.

 You may say that GHC should be cleverer, and push that type signature
 information into the application. And perhaps it should.  But you can
 never win. For example:
 {{{
   hard x = [ $$(printf "gluk" [|| "" ||]), undefined :: Char -> String ]
 }}}
 Here the RHS of `hard` is a 2-element list. Since all elements of a list
 have the same type, the splice must have the same type as the second
 element of the list, namely `Char->String`.  But seeing that would mean
 that we'd have to typecheck right-to-left.  In general GHC tries very very
 hard NOT to depend on traversal order.  There is no way in general to
 ensure that we have all the information now that constraint solving may
 ultimately produce.

 I'm not sure what to do about this.
  * It seldom matters, because resolving the overloading on the splice
 seldom depends on the result type.
  * When it does matter, you can fix it by giving a type signature to the
 splice itself.
 But it seems unsatisfactory.  Ideas welcome.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10271#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler