Checking constraints

[jkarni]

With:

t :: ('True ~ 'False) => Int
t = 5

shouldNotTypeCheck t fails (i.e., the test fails with "Expected expression to not compile but it did compile"). I see why this happens (deferring the type error happens to not cause an error), but the expression does not actually compile.

I can't say I know how this could be fixed...

[CRogers]

Hmm, I've never tried this with constraints before. Weird that it doesn't throw an a deferred type error and just lets you use it - I'm not sure what we can do to recognise that, as GHC seems to thinks it's fine code to run. Perhaps this is a GHC bug.

[jkarni]

I'm not sure I'd consider this a bug in GHC - I can see reasons to go either way here.

I have a couple of thoughts about how one might turn these into errors - I'll try them out soon and report back.

[CRogers]

I'm excited to see what you come up with!

[jkarni]

Hmm, I thought Deferrable could be the solution, but the p constraints don't unify during type inference, so that won't work.