Make forall keyword optional in instance declaration

[jrairigh]

Made the forall keyword optional in the instance header but gives warning if it is missing #1120. This change does not modify the actual meaning of the code. To do that, I believe the InstanceHead type would need to include a TypeForall type. This is a more difficult change than the ask for #1120, so hoping this can be worked in a separate issue.

[hdgarrood]

I would prefer not to make a change where the forall keyword is optional but has no effect, as I think that would be surprising and would not really provide the benefit that we would expect explicit quantification to provide here (specifically: helping you catch typos). I think if the keyword is present, then type variables should work the same way as they do in function declarations, so if there is a forall but the instance refers to a type variable which is not part of that forall, then that should be an error.

[jrairigh]

I'm unsure which type of error this would be. Is it one of these or a new type of error?

• QuantificationCheckFailureInKind Text

• QuantificationCheckFailureInType [Int] SourceType

• VisibleQuantificationCheckFailureInType Text

[garyb]

I'd say it should be a new error, since it's for an instance rather than a kind or type.

[jrairigh]

Something like QuantificationCheckFailureInInstanceHead?

[hdgarrood]

I'd suggest QuantificationCheckFailureInInstance. The phrase "instance head" sometimes refers to the entire part of the instance to the right of the =>, and sometimes refers just to the first type constructor appearing to the right of the =>. In either case I think that's not what we want here, because if you refer to an unbound type variable to the left of the =>, that should also cause this error; it applies to the whole instance.

[jrairigh]

Is the type non-terminal wanted before contraints "=>" or would that accept too much?

[rhendric]

You don't want the production to be type constraints '=>', not because it would accept too much, but because it would require an extra type expression before the constraints could be recognized (imagine forall a. (Maybe a) Show a =>, although in practice the situation would be further complicated by the fact that (Maybe a) Show a would in fact be parsed all as one type expression).

All you want to add to the production is forall many(typeVarBinding) '.', as seen in the production for type1.

[jrairigh]

The complication I'm running into with the forall many(typeVarBinding) '.' is that it's use in type1 maps to TypeForall which requires a type after the '.' -- Can I just pass in unit for this type or do I need to add a new Type constructor for this scenario?

[rhendric]

Locally, the right thing to do is probably to add another field to InstanceHead. Compare with how constraints are handled there: in a general type expression, the constraint would be wrapped up into a TypeConstrained, but that's not what happens in instHead. Instead, InstanceHead ends up somewhat awkwardly encoding a subset of the type language via Maybe and tuples, because not every type (Int -> String, for instance) would make a valid instance type. You want to extend that encoding, and just like with the constraint, you're not going to do that by reusing TypeForall, but instead by tupling up what would ordinarily go into the TypeForall.

[rhendric]

Alternatively, you could try blowing that encoding up and actually accepting any type in an instance head, but that might be more ambitious? I don't know what would happen if you tried that, and you might need to add in some extra errors somewhere else corresponding to the types that previously wouldn't parse.

[jrairigh]

Thanks @rhendric. I'll try option one first. Two questions:

1. Where would I find the code that detects and handles unbound type variables errors?
2. Is there a way I can rerun just failed test cases?

[rhendric]

1. The way to answer this kind of question is to find the appropriate error constructor in src/Language/PureScript/Errors.hs—in this case, that would be UndefinedTypeVariable—and then grep the code for where it's used—in this case, that leads me to lookupTypeVariable defined in src/Language/PureScript/TypeChecker/Monad.hs.
2. Not automatically, no. You can select specific tests manually on the command line by running stack test purescript --ta '-p NameOfATest'. If you want to run multiple tests in a single stack invocation, and they don't all have a word in common, you get to learn about Tasty's idiosyncratic implementation of awk patterns.

[jrairigh]

...explicit quantification to provide here (specifically: helping you catch typos). -- @hdgarrood

I'm trying to wrap my head around this so I can write good test cases but I can't think of a scenario where this would help catch a typo. I've tried two different ways, but in both examples the compiler already generates an error so I don't understand what adding forall syntax provides here. Can you please provide an example of situation forall syntax could help catch a typo?

Examples (borrowed from @michaelficarra),

-- error, because b is not an instance of Sized
instance sizedArray :: (Sized a) => Sized (List b) where
  size Nil = 0
  size (Cons x xs) = size x + size xs

-- error, no type class instance was found for t2, the instance head contains unknown type variables. Consider adding a type annotation.
instance sizedArray :: (Sized a, Sized b) => Sized (List a) where
  size Nil = 0
  size (Cons x xs) = size x + size xs

[hdgarrood]

The point is to generate an error which is more likely to help the user diagnose the problem as quickly as possible. While it is true that we do already generate an error in those cases, the point remains that it would often be more useful to generate a different one.

If that’s not persuasive enough then how about this:

class IsPositive number result
class IsPrime number result
instance checkPrimality ::
  ( IsPositive number True
  , -- [... other constraints to check whether `number` is actually prime ...]
  ) => IsPrime nubmer True

In which we are accidentally declaring that all numbers - even nonpositive ones - are prime due to a typo, because this primality test exists only at the type level and there are no term level expressions to help the compiler realise that something is off.

[jrairigh]

Thanks @hdgarrood. So adding forall to it like this --

class IsPositive number result
class IsPrime number result
instance checkPrimality :: forall number.
  ( IsPositive number True
  , -- [... other constraints to check whether `number` is actually prime ...]
  ) => IsPrime nubmer True

the compiler should generate error similar to how it would if it happened at the function level--
Type variable nubmer is undefined.

Is this the expectation?

[hdgarrood]

Yes, that's exactly right.

[jrairigh]

I added a new function, checkTypeQuantificationInInstance, in typeCheckAll, which looks to be the right place to report type errors --

Just typeClass -> do
          checkInstanceArity dictName className typeClass tys
          (deps', kinds', tys', vars) <- withFreshSubstitution $ checkInstanceDeclaration moduleName (sa, deps, className, tys)
          traverse_ checkTypeQuantificationInInstance tys'
          tys'' <- traverse replaceAllTypeSynonyms tys'

Problem is that tys' only contains the name of type implementing the typeclass -- 'nubmer' in code snippet provided by @hdgarrood. I assume that I will need to check that 'nubmer' is listed as one of the types in forall part, but I don't know how to get this. It looks like I'd need to add a new [SourceType] to the TypeInstanceDeclaration constructor for the forall types. However, this constructor is referenced in 14 different source files. Before I head down this path, I wanted to check there isn't a simpler solution I've overlooked?

[rhendric]

It looks like I'd need to add a new [SourceType] to the TypeInstanceDeclaration constructor for the forall types.

You might be better off adding a [(SourceAnn, Text, Maybe SourceType)] instead; you could encode the quantification variables as either a TypeVar or a KindedType wrapping a TypeVar, but that's a pretty small subset of SourceType to match against down the line. But yeah, adding a field to that constructor looks like the right thing to do to me.

[jrairigh]

For a test, I tried adding my quantification variable to the freeVars in checkInstanceDeclaration is Kinds.hs. I was hoping this would result in error since the type is TUnknown, but no error resulted. Couple questions:

1. Do the quantification checks go in checkInstanceDeclaration in Kinds.hs or should I put the check in a new function like checkQuantificationInInstanceDeclartaion?
2. and If so, are they free variables, type constraints, or a new category?

[jrairigh]

It's been awhile, but I'm back. @rhendric @garyb I have a passing test but not failing test. Couple questions:
Given a class,

1. Is it an error or warning if a type variable is brought into scope but not used? e.g.
2. Is it an error or warning if forall syntax is uses, but some variables are not quantified? e.g.

class Foo a where
   foo :: a

-- Warning or Error?
instance forall b. Foo (Maybe Int) where
   foo :: Maybe Int
   foo = Nothing

-- Warning or Error
instance forall b. Foo (Array a) where
   foo :: Array a
   foo = []

[garyb]

Welcome back 😄

I would say 1 is a warning, 2 is an error.

[JordanMartinez]

Just FYI. hdgarrood has stepped down from the core team.

[jrairigh]

@garyb @JordanMartinez
Do these cover all the test cases?
ebe8fac

[JordanMartinez]

There should be a failure output for this test. Could you push and commit that?

Also, I'd expect there to be 3 lines of -- @shouldFailWith ..., one for each error.

[JordanMartinez]

Similarly here, there should be a corresponding .out file. Can you commit and push that?

[jrairigh]

Will do. I'm guessing this will be easier to add once the compiler actually spits out an error :-D.

[JordanMartinez]

@garyb @JordanMartinez Do these cover all the test cases? ebe8fac

Not sure if this works or not but, is there a warning for a shadowed type variable?

instance forall a a. Foo a where
  ....

[JordanMartinez]

This line is out-of-date. Could you remove it and follow the directions in CHANGELOG.d/README.md?

[jrairigh]

@garyb @JordanMartinez Do these cover all the test cases? ebe8fac

Not sure if this works or not but, is there a warning for a shadowed type variable?

instance forall a a. Foo a where
  ....

Seems like reasonable assumption, but I entered this code into PSCi and it didn't give a warning.

> :paste
… shadowed :: forall a a. a -> Int
… shadowed _ = 0
> shadowed 0
0