Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Can TDNR do better on constructor matches? #5385

Open
ceedubs opened this issue Oct 1, 2024 · 0 comments
Open

Can TDNR do better on constructor matches? #5385

ceedubs opened this issue Oct 1, 2024 · 0 comments

Comments

@ceedubs
Copy link
Contributor

ceedubs commented Oct 1, 2024

Is your feature request related to a problem? Please describe.

I often run into error messages that tell me that a constructor name is ambiguous, but there is enough type information present that I would expect type-directed name resolution to be able to figure out what I mean without further qualification.

Example transcript input

```ucm
fresh/main> builtins.merge
```

```unison
type Type1 = MyConstructor Nat
type Type2 = MyConstructor Text

foo : Type1 -> Nat
foo = cases MyConstructor n -> n
```

Example transcript output

``` ucm
fresh/main> builtins.merge

  Done.

```
``` unison
type Type1 = MyConstructor Nat
type Type2 = MyConstructor Text

foo : Type1 -> Nat
foo = cases MyConstructor n -> n
```

``` ucm

  Loading changes detected in scratch.u.

  
    ❓
    
    I couldn't resolve any of these symbols:
    
        5 | foo = cases MyConstructor n -> n
    
    
    Symbol          Suggestions
                    
    MyConstructor   Type1.MyConstructor
                    Type2.MyConstructor
  

```



🛑

The transcript failed due to an error in the stanza above. The error is:


  
    ❓
    
    I couldn't resolve any of these symbols:
    
        5 | foo = cases MyConstructor n -> n
    
    
    Symbol          Suggestions
                    
    MyConstructor   Type1.MyConstructor
                    Type2.MyConstructor

Describe the solution you'd like

In this case there are two pieces of information present and I'd expect either one to be enough in isolation to remove ambiguity:

  • The input type has been specified as Type1, so I must be matching on a constructor of Type1.
  • The output type has been specified as Nat, so I must be matching on a constructor with a single Nat value.

The first item in particular seems like a strong signal to TDNR for pattern matches.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant