Opened 22 months ago

Closed 2 months ago

Last modified 2 months ago

#7021 closed feature request (fixed)

Tuple (and other exotic predicates) not yet handled in Template Haskell

Reported by: goldfire Owned by:
Priority: normal Milestone: 7.8.1
Component: Template Haskell Version: 7.5
Keywords: ConstraintKinds TemplateHaskell Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: th/T7021 Blocked By:
Blocking: Related Tickets:

Description

Say I make the following declarations:

{-# LANGUAGE ConstraintKinds #-}

type IOable a = (Show a, Read a)

foo :: IOable a => a
foo = undefined

It is currently impossible to reify foo in Template Haskell. This also comes up when using nested lists of constraints in Template Haskell quotes.

Change History (20)

comment:1 Changed 22 months ago by goldfire

For what it's worth, I do hope to look at implementing this feature sometime in the near future, but I wanted to document the feature request here first, and I may not get to it for a few weeks. Anyone else is, of course, welcome to take a stab.

comment:2 Changed 19 months ago by igloo

  • Difficulty set to Unknown
  • Milestone set to 7.8.1

Thanks for the report

comment:3 Changed 3 months ago by yoeight

Here's an implementation by introducing a new TH.Pred data constructor (let's say TypeT) as suggested by Richard here:

So, this is what I have in mind

  TypeT Type

By using the description's snippet, I got:

VarI Tuple.foo (ForallT [PlainTV a_1627398569] [TypeP (AppT (AppT (TupleT 2) (AppT (ConT GHC.Show.Show) (VarT a_1627398569))) (AppT (ConT GHC.Read.Read) (VarT a_1627398569)))] (VarT a_1627398569)) Nothing (Fixity 9 InfixL)

What do you think ?

Richard also suggested that we could make Pred a type synonym of TH.Type. Unfortunately, I have no idea how to express equality constraint only by using TH.Type

comment:4 Changed 3 months ago by goldfire

Do you mean TypeP in your example?

For my suggestion about making Pred a synonym of Type, we would need to add something like EqualityT to represent the poly-kinded equality predicate. Although this isn't a Haskell type, strictly speaking, there is already precedent for that in the constructors StarT and ConstraintT (which aren't types either).

I'm not sure which of these options (the TypeP or the synonym approach) is the better and would love to hear others' thoughts.

comment:5 Changed 3 months ago by simonpj

I rather agree with Richard: make Pred and Type into synonyms. That's what GHC does internally, and it works pretty well.

However that would be a bit of a bump: people's programs would break. A possible half-way house would be to have

data Pred = TypeP Type
  | ClassP Name [Type]
  | EqualP Type Type

and then deprecated ClassP and EqualP in favour of the equivalents in Type. Once that has settled down, making Pred into a synonym would still be a breaking change, but a very routine one to absorb.

Or it might be better to do it all at once. I'm not sure, and would welcome opinions.

Simon

comment:6 Changed 3 months ago by yoeight

Thanks for your advices !

I made Pred a type synonym of TH.Type.

Impacted files sum up:

dph-lifted-copy/Data/Array/Parallel/Lifted/TH/Repr.hs

compiler/hsSyn/Convert.lhs
compiler/typecheck/TcSplice.lhs

Language/Haskell/TH.hs
Language/Haskell/TH/Lib.hs
Language/Haskell/TH/Ppr.hs
Language/Haskell/TH/Syntax.hs

I have also made a test case based on description snippet

Yorick

comment:7 Changed 3 months ago by goldfire

Do you have patches posted somewhere? And I'm surprised that you didn't have to modify compiler/deSugar/DsMeta.lhs to get this working -- that file handles translation of TH quotes, which should support the new kinds of predicates. Where is your test case? Have you run the testsuite?

comment:8 Changed 3 months ago by yoeight

Surprisingly, I didn't have to modify DsMeta.lhs but I had to change a couple of test files that I've forgot in my sum up (respectively T8625.stdout and TH_genExLib.hs)

I did run the testsuite and everything is working properly

Patches can be found here.

Unfortunately, there were trailing whitespaces in some files

comment:9 follow-up: Changed 3 months ago by goldfire

This looks nice -- I can easily believe it works. Here is some feedback I have on the code:

  • I would want to see this handle IrredPred predicates, as well as tuples. That way, synonyms built with ConstraintKinds would be fully supported by TH. I don't think this should be too much work beyond what you've already done.
  • I still think a change to DsMeta is warranted. For example, I would imagine code like [t| (Show a, (Read a, Num a)) => a -> a |] would fail to compile, even though TH would now be able to represent such a predicate.
  • The functions classP and equalP in the Lib module are meant to echo the constructors of Pred. I would say that, now that Pred is a synonym, classP and equalP should be removed. (It took me a while to understand why all those functions are there in Lib -- the answer is that DsMeta is much easier to write with those functions there.) Leaving classP and equalP doesn't cause anyone any real harm, but it would just be a small wart on the design that could easily be eliminated.
  • Along similar lines, you will probably find that you need an equalityT function in Lib when updating DsMeta.
  • It looks like you left the old Pred commented-out in Syntax.
  • While it is probably too late now (and I don't think worth going back to fix), it's best to do whitespace changes in separate commits from substantive changes. Perhaps before editing a new file, removing the trailing whitespace, make a commit, and then go back and to the real changes. You can always then rebase at the end of your session to lump together all the whitespace commits.

Continued thanks for working on this!

comment:10 in reply to: ↑ 9 Changed 3 months ago by yoeight

Replying to goldfire:

This looks nice -- I can easily believe it works. Here is some feedback I have on the code:

  • I would want to see this handle IrredPred predicates, as well as tuples. That way, synonyms built with ConstraintKinds would be fully supported by TH. I don't think this should be too much work beyond what you've already done.

Do you have any pointer on what irreducible predicates are please ? If it's possible, could you provide a code sample that triggers irreducible predicate TH error ?

  • I still think a change to DsMeta is warranted. For example, I would imagine code like [t| (Show a, (Read a, Num a)) => a -> a |] would fail to compile, even though TH would now be able to represent such a predicate.

You were right, I got an error when compiling your code. I think we should use it in a new test case in order to increase code coverage. What do you think ?

  • The functions classP and equalP in the Lib module are meant to echo the constructors of Pred. I would say that, now that Pred is a synonym, classP and equalP should be removed. (It took me a while to understand why all those functions are there in Lib -- the answer is that DsMeta is much easier to write with those functions there.) Leaving classP and equalP doesn't cause anyone any real harm, but it would just be a small wart on the design that could easily be eliminated.
  • Along similar lines, you will probably find that you need an equalityT function in Lib when updating DsMeta.
  • It looks like you left the old Pred commented-out in Syntax.
  • While it is probably too late now (and I don't think worth going back to fix), it's best to do whitespace changes in separate commits from substantive changes. Perhaps before editing a new file, removing the trailing whitespace, make a commit, and then go back and to the real changes. You can always then rebase at the end of your session to lump together all the whitespace commits.

I agree. The thing is, I have (add-to-list 'write-file-functions 'delete-trailing-whitespace) in my .emacs. I didn't notice until I posted my patches.

Continued thanks for working on this!

Thanks for your feedback !

Yorick

comment:11 Changed 3 months ago by goldfire

The classification of predicates is done by classifyPredType, in the Type module. From the definition of that function, any predicate not headed by a class, equality predicate, or tuple is "irreducible". Examples of these include predicates headed by type families or predicates headed by variables. Both of these possibilities require ConstraintKinds.

Here is a full program that exhibits the problem:

{-# LANGUAGE TemplateHaskell, PolyKinds, ConstraintKinds #-}

module Irred where

import Language.Haskell.TH

data Proxy a = Proxy

foo :: a b => Proxy a -> b
foo = undefined

$( do info <- reify 'foo
      reportWarning (show info)
      return [] )

GHC 7.6.3 reports

    Can't represent irreducible predicates in Template Haskell: a b

Producing this error was admittedly harder than I thought. It turns out that TcSplice and DsMeta take rather different routes to translating into the TH syntax. (This is, of course, because TcSplice is translating from Core while DsMeta is translating from Haskell.) Only TcSplice checks the classification of predicates. Using a TH quote with an "irreducible" predicate produces a ClassP, even on a type like foo's type, above.

I hope this helps!

comment:12 Changed 3 months ago by yoeight

That did help a lot, thanks !

So, I (think) have implemented IrredPred. I have also fixed DsMeta.lhs, deleted classP, equalP and added equalityT

Sadly, I have a failing test testsuite/tests/perf/compiler/T4801.hs and I don't know how to work this out

Patches can be found here

Regards,

Yorick

comment:13 Changed 3 months ago by goldfire

Thanks for sharing your patch. Here are some further comments:

  • The EqualityT constructor has type Type -> Type -> Type. Yet, this would prevent encoding constructs like [t| ((~) Int) |], which should be valid. I recommend putting EqualityT in like ArrowT is now, as a nullary (0-argument) constructor.
  • The foldM and go algorithm (lines 65-67) you use seems like repTapps. Or, am I missing something?
  • In reifying an IrredPred, you use splitAppTy... but we're not sure there that the type is an application. For example, it could be a nullary type family, like this:
type family ALittleSilly :: Constraint

I believe this would be an IrredPred, if there are no instances for the type family. (I haven't tested it.)

I will say that I appreciate your attention to detail to GHC's coding style. I hope all these comments don't put you off -- we do really appreciate your contribution!

comment:14 Changed 3 months ago by yoeight

Thanks for your comments.

About foldM and go, I thought I could traverse tys and apply the resulted type in one pass. Using repTapps is not as direct. Anyway, I ported the code to repTapps as it seems more appropriate. foldM and go looked too obfuscated.

So as you suggested, EqualityT is now a nullary constructor and nullary type families are now supported. Let me now if there's any missing use case.

Thanks again for your concern and time, don't worry I don't need to be mothered :-). Being offended by helping comments would be inconsistent with my 'How ghc works ?' goal.

Updated patches are here

Also do you have any idea why testsuite/tests/perf/compiler/T4801.hs fails ? It's the only failure I got so far.

Regards,

Yorick

comment:15 Changed 2 months ago by Richard Eisenberg <eir@…>

In e0dadc87b57ce7f4ec3b72eb52e4abe5a5218f52/ghc:

Apply changes relative to TH.Pred becoming a TH.Type's synonym (issue #7021)

Signed-off-by: Richard Eisenberg <eir@cis.upenn.edu>

comment:16 Changed 2 months ago by Richard Eisenberg <eir@…>

In 182ff9e814a917681b1600b2729c3340801630de/ghc:

Fix tests due to issue #7021

Signed-off-by: Richard Eisenberg <eir@cis.upenn.edu>

comment:17 Changed 2 months ago by Richard Eisenberg <eir@…>

In 8e303d725eba0d6e0f9e52c64da21a0f299fa422/ghc:

Refactor previous commit on fixing #7021.

comment:18 Changed 2 months ago by goldfire

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to th/T7021

I've applied your patches, Yorick. I did a little refactoring at the end, but most of the code stood on its own. Many thanks!

I am not recommending this for merging, as it makes a non-trivial change to Template Haskell which will affect many users of TH. I think it's a move in the right direction, but I'm worried with the release candidate already out, that libraries will test against the RC, see that it works, and then be happy. If there's a user-facing change like this in 7.8, people could get caught unaware.

If anyone out there (particularly Yorick) feels differently, please advocate your case!

comment:19 Changed 2 months ago by carter

Could you summarize what sorts of TH would break with this change? Ie what gets broken vs what gets improved?

I assume the changes are localized to this commit https://ghc.haskell.org/trac/ghc/changeset/e0dadc87b57ce7f4ec3b72eb52e4abe5a5218f52/ghc mostly?

Could you expand on what sort of TH code might be impacted? (or should i find some time to build current head an test it on some project that currently support 7.8 RC and have heavy TH usage?)

comment:20 Changed 2 months ago by goldfire

Here is the relevant commit to TH:
http://git.haskell.org/packages/template-haskell.git/commitdiff/57b662c3efd8579595c8642fce2d4cd60ba4ec0b

In short, we've equated predicates with types (type Pred = Type) and added a new constructor to Type, EqualityT :: Type, which represents (~).

Thus, this would break any code that uses predicates in Template Haskell. That's a fair amount of breakage, but, as I said, I think this change is forward-thinking, especially given that predicates and types are the same type within GHC.

Note: See TracTickets for help on using tickets.