Impossible generic parameters shouldn't compile

[ynfle]

Generic that are constrained that have no possible resolution (T: SomeFloat and string) shouldn't compile

Example

proc t[T: SomeFloat and string](x: T): string =
  $x

Current Output

Compiles totally fine

Expected Output

Shouldn't compile

$ nim -v
Nim Compiler Version 1.5.1 [MacOSX: amd64]
Compiled at 2021-08-26
Copyright (c) 2006-2021 by Andreas Rumpf

git hash: c70e4040bd69e1ee32b6c676dbfc763c7cf4df37
active boot switches: -d:release

[timotheecour]

this would hurt generic code

when defined foo:
  type A = uint|int
else:
  type A = uint
proc f[T: A and int]()

[ynfle]

In the first case it should compile, but why should it compile in the second case? Is it not misleading to allow a proc that can't be called to compile? Maybe at least a compiler warning

[timotheecour]

for the same reason as we allow array[N, int] with N = 0: it's a corner case that can happen in generic code;

a warning might be acceptable

[ynfle]

But array[0, int] compiles and should compile

[ynfle]

Is it technically possible with the current type system to determine that there isn't an intersection between string & SomeFloat?

[Araq]

"possible", sure, probably but there is no problem to solve here. The error manifests as soon as you try to use the proc t, doesn't it.

[timotheecour]

there is no problem to solve here. The error manifests as soon as you try to use the proc t, doesn't it.

I cannot agree more.

note that, using the same argument, we don't need to type-check generics at declaration time (which causes many issues / complications, refs #8677 + similar issues with nimvm construct). Any attempt to instantiate the generic would trigger such issues. Refactorings that don't have that generic instantiated in a test suite could let errors slip by, but that's a moot argument given that it caters to code with poor test coverage, and more importantly, that generic prepass can only catch a small amount of the issues that could be found with generic instantiation, not to mention all the issues this causes (eg timotheecour#355 + others).

A generic pre-pass that restricts itself to symbol binding could be a possibly better design (there are ways to deal with scope injecting macros/templates called inside generics). link to recent discussion: https://discord.com/channels/371759389889003530/768367394547957761/880763539021791263

"possible", sure,

not possible in the general case, it ends up being a hard (possibly undecidable) constraint satisfaction problem, eg:

type A = concept x
  compiles(x.foo)
type B = concept x
  not compiles(x.foo)
proc main(a: A and B) = discard

I'm not even sure it's worth solving the "easy cases" (whatever that means); as mentioned in #18752 (comment), this would not work well in generic code.

[Araq]

we don't need to type-check generics at declaration time (which causes many issues / complications, refs #8677 + similar issues with nimvm construct)

I'm not sure what you mean here, I brought up type-checking of generics as a possible evolutionary path, but currently we don't do it at all and the pre-pass does only do symbol lookups.

[ynfle]

The error manifests as soon as you try to use the proc t, doesn't it.

However, the error message is misleading that the issue is at the callsite