Where's the imp... ?

[TimRichter]

Hello, idris 0.9.16 on Ubuntu 14.04 says

Type checking ./test.idr
test.idr:7:10:No such variable imp
Metavariables: Main.injTrans

when I ask it to typecheck this:

-- Injective Functions
data Injective : {a:Type} -> {b:Type} -> (f:(a->b)) -> Type where
  InjBy : ({x:a} -> {y:a} -> ((f x) = (f y)) -> (x = y)) -> 
          Injective {a = a} {b = b} f

injTrans : (Injective f) -> (Injective g) -> (Injective (f . g ))
injTrans (InjBy fInj) (InjBy gInj) = (InjBy fgInj) where
  fgInj pEq = gInj (fInj pEq)

I've also tried giving injTrans some more of the implicits, but idris just insists on that imp.

Please help! Tim

[edwinb]

'imp' (and variants) is the name given to the implicit lambda used to make 'f' typecheck.

Scoped implicits are a new feature, so there are likely to be weird issues and error messages like this popping up occasionally, but my guess is that the error is caused by the interaction of the argument 'fgInj' which uses a scoped implicit, and the fact that you haven't given a type declaration for the 'fgInj' in the where block.

I've been wondering if we should require type declarations in where blocks too, since the type inference there is limited. It's certainly unaware of things like scoped implicits at the moment.

If you try this:

   injTrans : (Injective f) -> (Injective g) -> (Injective (f . g ))
   injTrans (InjBy fInj) (InjBy gInj) = (InjBy ?fgInj)

And look at the type of fgInj:

   ...
   imp : a1
   imp1 : a1
--------------------------------------
fgInj : ((f . g) imp = (f . g) imp1) -> imp = imp1

Then this might suggest part of what's going on. I'll see if I can come up with a better way to report this error.

Edwin.

On 02/02/2015 16:44, Tim Richter wrote:

Hello, idris 0.9.16 on Ubuntu 14.04 says

Type checking ./test.idr test.idr:7:10:No such variable imp Metavariables: Main.injTrans

when I ask it to typecheck this:

|-- Injective Functions data Injective : {a:Type} -> {b:Type} -> (f:(a->b)) -> Type where InjBy : ({x:a} -> {y:a} -> ((f x) = (f y)) -> (x = y)) -> Injective {a = a} {b = b} f

injTrans : (Injective f) -> (Injective g) -> (Injective (f . g )) injTrans (InjBy fInj) (InjBy gInj) = (InjBy fgInj) where fgInj pEq = gInj (fInj pEq) |

I've also tried giving injTrans some more of the implicits, but idris just insists on that imp.

Please help! Tim

— Reply to this email directly or view it on GitHub https://github.com/idris-lang/Idris-dev/issues/1887.

[TimRichter]

Thanks Edwin, that's too much guesswork for the typechecker, I see. This:

-- Injective Functions
data Injective : (f:(a->b)) -> Type where
  InjBy : ({x:a} -> {y:a} -> ((f x) = (f y)) -> (x = y)) -> Injective {a = a} {b = b} f

compInjIsInj : {f:(b -> c)} -> {g:(a->b)} -> (Injective f) -> (Injective g) -> (Injective (f . g ))
compInjIsInj  (InjBy {a = b} {b = c} {f = f} fInj) 
              (InjBy {a = a} {b = b} {f = g} gInj) = 
              (InjBy {a = a} {b = c} {f = f . g} fgInj) where
     fgInj : {x:a} -> {y:a} -> ((f (g x)) = (f (g y))) -> (x = y)
     fgInj pEq = gInj (fInj pEq)

works and is still kind of readable.

As you wrote, the type declaration for fgInj is the crucial thing.

I'll close the issue. Best, Tim