? implicit in pattern match is unsound

idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.5k stars 375 forks source link

? implicit in pattern match is unsound #1031

Open mb64 opened 3 years ago

mb64 commented 3 years ago

Steps to Reproduce

total
ohNo : Void
ohNo = let (? ** x) = the (a ** a) (Int ** 5) in x

Expected behavior

This should not compile.

Observed Behavior

Idris2 unifies the implicit hole with the expected type Void, even though it should be a bound/skolem variable, not able to change for unification.

$ idris2 --no-banner t.idr
Main> :t ohNo
Main.ohNo : Void
Main> :total ohNo
Main.ohNo is total
Main> ohNo
5

mb64 commented 3 years ago

? seems to behave identically to .(_) in patterns, so it would not solve the problem to disallow ? in patterns entirely.

-- These compile (bad)
foo : (x : Bool) -> So x
foo = \ ? => Oh

bar : (x : Bool) -> So x
bar = \ .(_) => Oh

-- These don't compile (good)
cool : (x : Bool) -> So x
cool ? = Oh

nice : (x : Bool) -> So x
nice .(_) = Oh

mb64 commented 3 years ago

Fixing this will require keeping much more precise track of which metavariables need to be resolved by when. Here is another issue that having this more precise info would hopefully fix:

-- Correctly succeeds: infers the lambda to have type Int -> Int
id1 : ?
id1 = \x => the Int x

-- Incorrectly fails: after processing the LHS, asserts that all metavars are already solved
id2 : ?
id2 x = the Int x