Opened 5 years ago

Last modified 9 months ago

#10271 new bug

Typed Template Haskell splice difficulty when resolving overloading

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 7.10.1
Keywords: TypedTemplateHaskell Cc: garrett
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

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:

    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.

Change History (6)

comment:1 Changed 5 years ago by simonpj

Description: modified (diff)

comment:2 Changed 5 years ago by garrett

Cc: garrett added

comment:3 Changed 4 years ago by thomie

Component: CompilerTemplate Haskell

comment:4 Changed 4 years ago by goldfire

Component: Template HaskellCompiler (Type checker)

This has much more to do with the overall type-checking algorithm than with Template Haskell.

comment:5 Changed 9 months ago by mpickering

Keywords: TypedTemplateHaskell added

comment:6 Changed 9 months ago by goldfire

Component: Compiler (Type checker)Template Haskell
Note: See TracTickets for help on using tickets.