Auto-implicit search fails with continuous data constructor parameter

[xiaoyangzhuang]

Example.txt

Auto-implicit search fails if the desired data constructor has a continuous parameter (e.g. DataConstructor2 : Double -> Type2). However, search succeeds if the parameter is discrete (e.g. DataConstructor2 : Bool -> Type2).

Steps to Reproduce

1. Copy the following into a .idr file:

data Type1 : Type where
    DataConstructor1 : Bool -> Type1

data Type2 : Type where
    DataConstructor2 : Double -> Type2

-- Works great!
function1 : {auto prf : Type1} -> IO ()
function1 = printLn "Auto-implicit parameter found successfully!"

-- Fails
function2 : {auto prf : Type2} -> IO ()
function2 = printLn "Auto-implicit parameter not found."

2. On the REPL, hit the following:
   :exec function1
:exec function2

Expected Behavior

:exec function1 => "Auto-implicit parameter found successfully!"
:exec function2 => "Auto-implicit parameter not found."

Observed Behavior

:exec function1 behaves as expected.
:exec function2 => Incomplete term ([__])