Opened 7 months ago

Closed 6 weeks ago

Last modified 5 weeks ago

#15471 closed bug (fixed)

Polymorphism, typed splices and type inference don't mix

Reported by: mpickering Owned by:
Priority: normal Milestone: 8.8.1
Component: Template Haskell Version: 8.4.3
Keywords: TypedTemplateHaskell Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: th/T15471
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5286, https://gitlab.haskell.org/ghc/ghc/merge_requests/106
Wiki Page:

Description

Trying to quote and splice a polymorphic function doesn't work unless you have a type signature.

{-# LANGUAGE TemplateHaskell #-}
module A where

foo1 x = x

test_foo = [|| foo1 ||]
{-# LANGUAGE TemplateHaskell #-}
module B where

import A

qux = $$(test_foo)

The type of qux is Any -> Any! Which is clearly wrong.

Adding a type signature to qux fixes the problem.

qux :: a -> a
qux = $$(test_foo)

Either there should be a better error or this should just work.

It seems that this has always been broken. Ryan tested on GHC 7.8.4 for me.

Change History (20)

comment:1 Changed 7 months ago by RyanGlScott

Component: CompilerTemplate Haskell
Type of failure: None/UnknownGHC rejects valid program

comment:2 Changed 7 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:3 Changed 6 months ago by mpickering

Anyone have any ideas about this? Perhaps Simon?

comment:4 Changed 6 months ago 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.

comment:5 Changed 6 months ago by mpickering

I still claim there is some bug here for two reasons.

  1. The result is unusable after splicing.
  2. A very similar program using static pointers works fine.
foo = static (id :: forall a . a -> a ) 

foo2 = [|| id :: forall a . a -> a ||] 

In GHCi

> (deRefStaticPtr foo) 'a'
'a'

> ($$(foo2)) 5

<interactive>:89:12: error:
    • No instance for (Num Any) arising from the literal ‘5’
    • In the first argument of ‘$$(foo2)’, namely ‘5’
      In the expression: ($$(foo2)) 5
      In an equation for ‘it’: it = ($$(foo2)) 5

comment:6 Changed 6 months ago 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)

comment:7 Changed 6 months ago by mpickering

Metaocaml also does the right thing here for what it's worth.

# let id x = x;; 
val id : 'a -> 'a = <fun>
# let t = .< id >.;;
val t : ('a -> 'a) code = .<(* CSP id *)>. 
# let v = (!. t) 5;;
val v : int = 5

comment:8 in reply to:  6 Changed 6 months ago by mpickering

Replying to 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.

comment:9 Changed 6 months ago by simonpj

I think that the type of the quote is fine

What type do you expect test_foo to have?

comment:10 Changed 6 months ago by mpickering

test_foo should have type forall a . Q (TExp (a -> a)).

Which is the same as in metaocaml.

comment:11 Changed 6 months ago by simonpj

But that doesn't scale well

foo2 :: Num a => a -> a
foo2 x = x+1

test_foo2 :: ???
test_foo2 = [|| foo2 |]]

If you give it the type test_foo2 :: forall a. Num a => Q (TExp (a->a)) then you'll need to decide what dictionary to pass to it when you invoke it in $$(test_foo2).

Only erasure is allowing MetaOCaml to squeeze by, and we don't have that luxury.

comment:12 Changed 6 months ago 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.

comment:13 Changed 6 months ago by simonpj

Yes, GHC infers test_foo2 :: forall a. Num a => Q (TExp (a->a)). You like that -- good.

But now what would you expect to happen here?

qux = $$(test_foo2)

We must pass a dictionary, so we probably default to Integer. And that's precisely what is happening in the Description, except that there we default to Any because we don't have to satisfy Num.

comment:14 Changed 5 months ago 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.

comment:15 Changed 5 months ago by goldfire

I vote for the zonker, if only because the zonker is still in the TcM monad, making (3) above easier. Otherwise, the desugarer has to call the type checker, which is awkward.

comment:16 Changed 4 months ago by mpickering

Differential Rev(s): Phab:D5286

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.

comment:17 Changed 8 weeks ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:18 Changed 6 weeks ago by RyanGlScott

Differential Rev(s): Phab:D5286Phab:D5286, https://gitlab.haskell.org/ghc/ghc/merge_requests/106
Milestone: 8.10.18.8.1
Resolution: fixed
Status: newclosed
Test Case: th/T15471

Landed in c2455e647501c5a382861196b64df3dd05b620a2:

commit c2455e647501c5a382861196b64df3dd05b620a2
Author: Matthew Pickering <matthewtpickering@gmail.com>
Date:   Wed Jan 9 14:52:30 2019 +0000

    Run typed splices in the zonker
    
    Summary:
    This fixes #15471
    
    In the typechecker we check that the splice has the right type but we
    crucially don't zonk the generated expression. This is because we might
    end up unifying type variables from outer scopes later on.
    
    Reviewers: simonpj, goldfire, bgamari
    
    Subscribers: rwbarton, carter
    
    GHC Trac Issues: #15471
    
    Differential Revision: https://phabricator.haskell.org/D5286

comment:19 Changed 6 weeks ago by mpickering

Keywords: TypedTemplateHaskell added

comment:20 Changed 5 weeks ago by Matthew Pickering <matthewtpickering@…>

In c2455e64/ghc:

Run typed splices in the zonker

Summary:
This fixes #15471

In the typechecker we check that the splice has the right type but we
crucially don't zonk the generated expression. This is because we might
end up unifying type variables from outer scopes later on.

Reviewers: simonpj, goldfire, bgamari

Subscribers: rwbarton, carter

GHC Trac Issues: #15471

Differential Revision: https://phabricator.haskell.org/D5286
Note: See TracTickets for help on using tickets.