No -Wbadly-staged-types warning for required type argument

added Plow Tbug TemplateHaskell visible dependent quantification labels

Very true @monoidal , the warning should trigger on this example as well.

Could @int-index or @sand-witch look into this perhaps?

changed milestone to %9.10.2

As I can see, this check lives in rnHsTyKi env tv@(HsTyVar _ ip (L loc rdr_name)) case, in this statement:

; when (nameIsLocalOrFrom this_mod name) $
  checkThLocalTyName name

However, we don't have such information about visible type arguments at renaming pass. Perhaps, we need to add the same check inside a expr_to_type transformation.

Actually, there are a lot of other checks that can be bypassed with expr_to_type transformation!

Consider this code:

{-# LANGUAGE RequiredTypeArguments, 
             TypeAbstractions, 
             AllowAmbiguousTypes #-}

import Data.Data
import GHC.TypeLits

main :: IO ()
main = do
  print (natViz 42)
  -- print (nat @42)

natViz :: forall a  -> KnownNat a => Integer
natViz n = natVal (Proxy @n)

nat :: forall a. KnownNat a => Integer
nat @n = natVal (Proxy @n)

print (natViz 42) complies just fine, whether print (nat @42) is a hard error:

    Illegal type: ‘42’
    Suggested fix: Perhaps you intended to use DataKinds
   |
10 |   print (nat @42)
   |               ^^

We don't check that a type literal is non-negative, so this code hangs indefinitely with eating more and more memory:

{-# LANGUAGE RequiredTypeArguments,
             TypeAbstractions,
             AllowAmbiguousTypes,
             LexicalNegation #-}

import Data.Data
import GHC.TypeLits

main :: IO ()
main = do
  print (natViz (-42))

natViz :: forall a  -> KnownNat a => Integer
natViz n = natVal (Proxy @n)

It also can bypass NoKindSignatures extension. But this is a minor issue comparing to others.

There are some checks of PolyKinds missing.

Ugh, and the same applicable to pat_to_type transformation...

Quite right.

These errors are emitted by the renamer but the output of the T2T transform is fed only to the desugarer.

The right solution is, I think, is to move these checks from the renamer to the typechecker. That would probably be fiddly but not hard.

mentioned in issue #24783

For TTH, splice i.e.

g :: forall a -> Code Q (a -> a)
g a = [|| idVis a ||]

I agree that all checks should be done in type-checker. It's typed template haskell.

But for untyped quotation, like

g a :: forall a -> ExpQ
g a = [| idVis a |]

it's a lot trickier. I guess it simply doesn't (cannot?) work:

Prelude Language.Haskell.TH> let idVis :: forall a -> a -> a; idVis _ x = x
Prelude Language.Haskell.TH> let f :: forall a -> ExpQ; f a = [| idVis a |] in f Char
<interactive>:11:34: error: [GHC-01928]
    • Illegal term-level use of the type variable ‘a’

and we must use [| idVis (type a) |] syntax. There aren't types to hint the right interpretation. And then we can do the check in renamer, where arguably, we have to do all the untyped-TH stuff.

I'd add this issue as an example of fundamental differences between TH and TTH. It's somewhat clear how this should work in TTH, but complete mystery whether it can work in TH at all.

EDIT: I view TH and TTH as separate systems, even if they share implementation machinery. As language features, "macros" and "typed staging" are very different, and their design and development shouldn't be constrained by each other.

I recently discussed a very similar issue with Andràs Kovacs. We more or less came to the conclusion that

g :: forall a -> Code Q (a -> a)
g a = [|| idVis a ||]

should be rejected; if only for the simple reason that cross-stage persistence doesn't work for locally-bound variables.

The usual way to work around that on the term-level is by using lift. Alas, for types we do not really have Lift!

For constraints, CodeC was proposed to lift (or persist?) constraints to the next stage. For types, we do not even have retained evidence to begin with! One more reason to have CodeT

g :: forall a -> CodeT Q a => Code Q (a -> a)
g a = [|| idVis a ||]

I guess CodeT Q a would be implied by Typeable a.

The exact design does not really have anything to do with the OP, but the point is that I tend to agree with the discussion so far that -Wbadly-staged-types should trigger.

@sgraf812

... should be rejected;

that's orthogonal. In !11081 (closed) my first intention was to make this kind of code rejecteted. But it changes which programs are accepted (in particular, would required changes to tests in test-suite), so needs a GHC proposal, and I'm not writing one.

This issue is that RequiredTypeArguments use-case is not recognised. If were recognised, you may than decide what to do, warn, error or lift etc.

I guess CodeT Q a would be implied by Typeable a.

CodeT Q a and Typeable are very similar, however, but the long story short, the "evidence" they carry is different enough, that it's probably better to not tie them together. (In particular, RankNTypes and ImpredicativeTypes has no chance to work with current Typeable, but it's easy enough to imagine use cases where forall a -> ... is instantiated with a polytype).

"Literature" calls that constraint LiftT (Typeable), and (probably only I at this point) reserve the name CodeT for the analogue of TypeRep - the actual evidence. See https://hackage.haskell.org/package/codet. The little experience I gathered from using that, is that CodeT backed up by Q TH.Type mostly works. And only mostly works for the same reason the rest of TTH mostly works: because Code Q a is backed by Q Exp, and that's not good enough.

changed milestone to %9.10.3

No -Wbadly-staged-types warning for required type argument

Child items ...

Activity