Can't solve constraints in values which came from constructor binders where the constructor was polymorphic

[jy14898]

Before this change, you couldn't solve constraints in values which came from constructor binders where the constructor was polymorphic:

class Con

newtype Identity a = Identity a

-- works
test1 :: Con => (Con => Int) -> Int
test1 a = a

-- fails
test2 :: Con => Identity (Con => Int) -> Int
test2 (Identity a) = a

This is because we weren't applying substitutions when checking the types of 'Var' exprs before subsumption, and polymorphic types like Identity get instantiated with unknowns during binder inference. This change adds the substitution in.

Checklist:

• Added a file to CHANGELOG.d for this PR (see CHANGELOG.d/README.md)
• Added myself to CONTRIBUTORS.md (if this is my first contribution)
• Linked any existing issues or proposals that this pull request should close
• Updated or added relevant documentation
• Added a test for the contribution (if applicable)

[garyb]

I can't think of a reason why there would be a problem doing this. Those revised error output seem like improvements too! 👍

[rhendric]

How exactly does this get used? I've tried adding:

instance Con

x = test (Identity (2 :: Con => Int))

and I get:

         Could not match constrained type
                     
           Con => Int
                     
         with type
              
           Int
              
       
       while trying to match type Int
         with type Con => Int
       while checking that expression Identity 2
         has type Identity (Con => Int)
       in value declaration main

Is there a different way to construct values with constrained types that can be used in polymorphic constructors, and if not, is this feature then incomplete?

[jy14898]

How exactly does this get used?

Good point, originally I was just messing around with deferring execution of expressions automatically (similar to https://github.com/natefaubion/purescript-call-by-name I believe), and found it surprising that using Identity would not work.

I was using FFI to construct these values which meant I never actually tested creating them in-language.

I'll have a look to see if it makes sense to allow constructing such values naturally

[jy14898]

@rhendric It's possible, although you have to be explicit about the type of Identity when constructing it:

-- compiles fine in the pull req, with inferred type Con => Int
test2' = test2 ((Identity :: (Con => Int) -> Identity (Con => Int)) 10)

The changes required to not need that hint are too great, I think

It's actually possible to write the original test2 with hints that works without the PR, although it'd defeat the purpose of my original use, which was to have such a function be simple to write:

test2 :: Con => Identity (Con => Int) -> Int
test2 (Identity (a :: Con => Int)) = a

[rhendric]

What about:

test :: Con => { foo :: Con => Int } -> Int
test x = x.foo

Is there a way to annotate that to make it work?

Then there's this little puzzle:

-- doesn't work
unid1 :: Identity (Con => Int) -> (Con => Int)
unid1 = coerce

-- works
unid2 :: Identity (Con => Int) -> (Con => Int)
unid2 = coerce :: forall a. Identity a -> a

I guess I'm broadly concerned that the whole impredicative types question hasn't been exhaustively thought out in PureScript (considering interactions with function types, data constructors and destructors, records, arrays, anything else that gets somewhat special handling that I'm missing right now), and even though this seems like a harmless and, to a limited audience, beneficial enhancement to type inference, I'm not confident that it implements, or gets us closer to, a set of inference rules that would be straightforward to explain to a learner. It could easily be that in that respect, this change doesn't make the situation any worse—I'm just asking the broad question and hoping that someone with a stronger type theory background can say that it does or doesn't.