Mysterious type mismatch between @@constructors. Interfaces striking back again?

[nicolabotta]

The code

> module NumProperties

> import Data.Fin
> import Data.Vect
> import Syntax.PreorderReasoning

> %default total
> %access public export

> interface (Num t) => NumMultZeroOne t where
>   multZeroRightZero   : (x : t) -> x * 0 = 0
>   multZeroLeftZero    : (x : t) -> 0 * x = 0
>   multOneRightNeutral : (x : t) -> x * 1 = x
>   multOneLeftNeutral  : (x : t) -> 1 * x = x

> interface (Num t) => NumMultDistributesOverPlus t where
> -- interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where
>   multDistributesOverPlusRight : (x, y, z : t) -> x * (y + z) = (x * y) + (x * z)
>   multDistributesOverPlusLeft  : (x, y, z : t) -> (x + y) * z = (x * z) + (y * z)

> multSV : (Num t) => t -> Vect m t -> Vect m t
> multSV x = map (x *)

> postulate sumLemma : (Num t) => (x : t) -> (xs : Vect m t) -> sum (x :: xs) = x + sum xs

> multSumLemma : (NumMultZeroOne t, NumMultDistributesOverPlus t) =>
> -- multSumLemma : (NumMultDistributesOverPlus t) =>
>                (x : t) -> (xs : Vect m t) ->
>                x * sum xs = sum (multSV x xs)
> multSumLemma x  Nil      = ( x * (fromInteger 0) )
>                          ={ multZeroRightZero x }=
>                            ( fromInteger 0 )
>                          ={ Refl }=
>                            ( sum Data.Vect.Nil )
>                          QED
> multSumLemma x (y :: ys) = ( x * (sum (y :: ys)) )
>                          ={ cong (sumLemma y ys) }=
>                            ( x * (y + sum ys) )
>                          ={ multDistributesOverPlusRight x y (sum ys) }=
>                            ( (x * y) + (x * sum ys) )
>                          ={ cong (multSumLemma x ys) }=
>                            ( x * y + sum (multSV x ys) )
>                          ={ sym (sumLemma (x * y) (multSV x ys)) }=
>                            ( sum (x * y :: multSV x ys) )
>                          ={ Refl }=
>                            ( sum (multSV x (y :: ys)) )
>                          QED

Fails to type check with

- + Errors (1)
 `-- NumProperties.lidr line 30 col 27:
     When checking right hand side of multSumLemma with expected type
             x * sum [] = sum (multSV x [])

     When checking argument x to function Syntax.PreorderReasoning.Equal.step:
             Type mismatch between
                     (@@constructor of NumProperties.NumMultZeroOne#Num t) (Inferred value)
             and
                     (@@constructor of NumProperties.NumMultDistributesOverPlus#Num t) (Given value)

             Specifically:
                     Type mismatch between
                             (@@constructor of NumProperties.NumMultZeroOne#Num t)
                     and
                             (@@constructor of NumProperties.NumMultDistributesOverPlus#Num t)

But replacing

> interface (Num t) => NumMultDistributesOverPlus t where
> -- interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where

with

> -- interface (Num t) => NumMultDistributesOverPlus t where
> interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where

and

> multSumLemma : (NumMultZeroOne t, NumMultDistributesOverPlus t) =>
> -- multSumLemma : (NumMultDistributesOverPlus t) =>

with

> -- multSumLemma : (NumMultZeroOne t, NumMultDistributesOverPlus t) =>
> multSumLemma : (NumMultDistributesOverPlus t) =>

makes the code type check fine! Perhaps an error in the implementation of interfaces?

[TimRichter]

Hi Nicola, hi all,

it seems Idris doubts that the two Num-implementations presupposed by (NumMultZeroOne t)
and (NumMultDistributesOverPlus t) are the same.

This doesn't fit with the general idea of interfaces as given in the tutorial, where one reads:

Only one implementation of an interface can be given for a type — implementations may not overlap.

On the other hand, looking at the types, e.g.

*NumProperties> :printdef NumMultZeroOne
data NumMultZeroOne : (t : Type) -> Type where
  constructor of NumProperties.NumMultZeroOne : {t : Type} -> Prelude.Interfaces.Num t =>
    (multZeroRightZero : (x : t) ->
        (=) {A = t} {B = t} (Prelude.Interfaces.(*) {ty = t} {{constraint}} x 0) 0) ->
    (multZeroLeftZero : ...) ->
    ...
     -> NumProperties.NumMultZeroOne t

one finds that the (Num t) implementations are just (constraint ... but what exactly does this mean?) arguments to the constructors of data types ... and the error message becomes kind of understandable.

I'd wish someone could come up with a more in depth introduction to how interfaces work,
covering in particular

• how to deal with nonlinear hierarchies of interfaces (as here),
• how to work with named instances,
• how to write functions with constraints when auto_implicits are off.

Btw, when adding an explicit (Num t) constraint to multSumLemma

> multSumLemma : (Num t, NumMultZeroOne t, NumMultDistributesOverPlus t) =>

the error message becomes really funny (showimplicits switched on):

...
When checking an application of function Syntax.PreorderReasoning.Equal.step:
        Type mismatch between
                (=) {A = t}
                    {B = t}
                    0
                    0 (Type of Syntax.PreorderReasoning.Equal.qed {a = t} 0)
        and
                (=) {A = t} {B = t} 0 0 (Expected type)

        Specifically:
                Type mismatch between
                        0
                and
                        0

Ciao,
Tim

[edwinb]

This is the same as #2497 - if you have x : Num t and y : Num t, you can't deduce that x = y because of the presence of named implementations. Also, even if we didn't have named instances, you still couldn't deduce x = y because it would still be possible to construct a different instance via the core language.
So if you have some diamond shaped hierarchy, there's no guarantee you'll arrive at the same instance at the top.

What the tutorial should say is that non-named implementations cannot overlap.

Essentially, interfaces are records with a handy syntax for the very common case of overloading names. If you need a lot of control, perhaps you should be using records instead.

[nicolabotta]

Edwin, I would expect problems with diamond shaped hierarchies or multiple inheritance to possibly trigger "can't disambiguate" errors, not "type mismatch" errors. It also seems to me that such errors should be avoidable by enforcing more strict visibility rules. Here (as in #2497), however, we seem to be facing a more elementary problem: the program

> module NumProperties

> import Data.Fin
> import Data.Vect
> import Syntax.PreorderReasoning

> %default total
> %access public export

> interface (Num t) => NumMultZeroOne t where
>   multZeroRightZero   : (x : t) -> x * 0 = 0
>   multZeroLeftZero    : (x : t) -> 0 * x = 0
>   multOneRightNeutral : (x : t) -> x * 1 = x
>   multOneLeftNeutral  : (x : t) -> 1 * x = x

> -- interface (Num t) => NumMultDistributesOverPlus t where
> interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where
>   multDistributesOverPlusRight : (x, y, z : t) -> x * (y + z) = (x * y) + (x * z)
>   multDistributesOverPlusLeft  : (x, y, z : t) -> (x + y) * z = (x * z) + (y * z)

> multSV : (Num t) => t -> Vect m t -> Vect m t
> multSV x = map (x *)

> postulate sumLemma : (Num t) => (x : t) -> (xs : Vect m t) -> sum (x :: xs) = x + sum xs

> -- multSumLemma : (NumMultZeroOne t, NumMultDistributesOverPlus t) =>
> multSumLemma : (NumMultDistributesOverPlus t) =>
>                (x : t) -> (xs : Vect m t) ->
>                x * sum xs = sum (multSV x xs)
> multSumLemma x  Nil = trans s1 (trans s2 (trans s3 s4)) where
>   s1 : x * sum Nil = x * fromInteger 0
>   s1 = Refl
>   s2 : x * fromInteger 0 = fromInteger 0
>   s2 = multZeroRightZero x
>   s3 : fromInteger 0 = sum Nil
>   s3 = Refl
>   s4 : sum Nil = sum (multSV x Nil)
>   s4 = Refl
> multSumLemma x (y :: ys) = trans s1 (trans s2 (trans s3 (trans s4 s5))) where
>   s1 : x * (sum (y :: ys)) = x * (y + sum ys)
>   s1 = cong (sumLemma y ys)
>   s2 : x * (y + sum ys) = (x * y) + (x * sum ys)
>   s2 = multDistributesOverPlusRight x y (sum ys)
>   s3 : (x * y) + (x * sum ys) = x * y + sum (multSV x ys)
>   s3 = cong (multSumLemma x ys)
>   s4 : x * y + sum (multSV x ys) = sum (x * y :: multSV x ys)
>   s4 = sym (sumLemma (x * y) (multSV x ys))
>   s5 : sum (x * y :: multSV x ys) = sum (multSV x (y :: ys))
>   s5 = Refl

fails now to type check (with 0.11-git:7e7d0eb) with

- + Errors (1)
 `-- NumProperties.lidr line 31 col 5:
     When checking type of NumProperties.multSumLemma, s1:
     When checking an application of function Prelude.Interfaces.*:
             t is not a numeric type

which seems an Idris bug to me. Ciao, Nicola

[nicolabotta]

So if you have some diamond shaped hierarchy, there's no guarantee you'll arrive at the same instance at the top.

Could some of the problems with diamond shaped hierarchies be alleviated by requiring declarations like

interface (Foo t) => Bar t where
interface (Foo t, Bar t) => Dee t where

whenever Foo features need to be accessible for Deemethods?

[edwinb]

This turns out to be a problem with error messages. I'm on a bit of a mission to improve error messages at the minute too... The real error in the code snippet above can be minimised to this definition:

s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
s1 = Refl

The problem is that it doesn't know whether you mean Vect.Nil or List.Nil, and this causes a chain of other things not being resolved. I'll see if I can find a way to get it to report that instead, since it is the real error...

[nicolabotta]

The real error in the code snippet above can be minimised to this definition:

s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
s1 = Refl

The problem is that, if one disambiguates all Nils by hand

> multSumLemma x  Nil = trans s1 (trans s2 (trans s3 s4)) where
>   s1 : x * sum Data.Vect.Nil = x * fromInteger 0
>   s1 = Refl
>   s2 : x * fromInteger 0 = fromInteger 0
>   s2 = multZeroRightZero x
>   s3 : fromInteger 0 = sum Data.Vect.Nil
>   s3 = Refl
>   s4 : sum Data.Vect.Nil = sum (multSV x Data.Vect.Nil)
>   s4 = Refl

, one ends up with

- + Errors (1)
 `-- NumProperties.lidr line 31 col 48:
     When checking right hand side of multSumLemma with expected type
             x * sum [] = sum (multSV x [])

     When checking an application of function trans:
             Type mismatch between
                     sum [] =
                     sum (multSV x []) (Type of NumProperties.multSumLemma, s4 t
                                                                               x
                                                                               constraint)
             and
                     0 = 0 (Expected type)

             Specifically:
                     Type mismatch between
                             0
                     and
                             0

! The problem does not disappear if one defines multSV via pattern matching:

> multSV : (Num t) => t -> Vect m t -> Vect m t
> -- multSV x = map (x *)
> multSV x  Nil      = Nil
> multSV x (y :: ys) = (x * y) :: (multSV x ys)

[edwinb]

Most likely the numeric types are different. I wonder if the defaulting
mechanism is kicking in and making one of the literals an Integer
because there's no immediate context to suggest otherwise (remembering
that = is heterogeneous).

I might turn that mechanism off, it probably causes more harm than good,
except at the REPL, and we can still allow it at the REPL anyway.

On 20/04/2016 11:36, nicolabotta wrote:

The real error in the code snippet above can be minimised to this definition:

s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
s1 = Refl

The problem is that, if one disambiguates all Nils by hand

> multSumLemma x  Nil = trans s1 (trans s2 (trans s3 s4)) where
>   s1 : x * sum Data.Vect.Nil = x * fromInteger 0
>   s1 = Refl
>   s2 : x * fromInteger 0 = fromInteger 0
>   s2 = multZeroRightZero x
>   s3 : fromInteger 0 = sum Data.Vect.Nil
>   s3 = Refl
>   s4 : sum Data.Vect.Nil = sum (multSV x Data.Vect.Nil)
>   s4 = Refl

, one ends up with

- + Errors (1)
 `-- NumProperties.lidr line 31 col 48:
     When checking right hand side of multSumLemma with expected type
             x * sum [] = sum (multSV x [])

     When checking an application of function trans:
             Type mismatch between
                     sum [] =
                     sum (multSV x []) (Type of NumProperties.multSumLemma, s4 t
                                                                               x
                                                                               constraint)
             and
                     0 = 0 (Expected type)

             Specifically:
                     Type mismatch between
                             0
                     and
                             0

! The problem does not disappear if one defines multSV via pattern matching:

> multSV : (Num t) => t -> Vect m t -> Vect m t
> -- multSV x = map (x *)
> multSV x  Nil      = Nil
> multSV x (y :: ys) = (x * y) :: (multSV x ys)

---

You are receiving this because you commented.
Reply to this email directly or view it on GitHub:
#3078 (comment)

[nicolabotta]

You are probably right Edwin! Setting showimplicits reveals that the given equality is homogeneous but the expected one is heterogeneous, for what I understand. Best, Nicola

[ahmadsalim]

To be honest, I think that diamond shaped hierarchies would nice to have solved. I am experiencing some issues with this as well especially when one tries to have things like Verified* interfaces of everything, i.e. Functor f => VerifiedFunctor f and Applicative f, VerifiedFunctor f => VerifiedApplicative f, where the latter would easily create diamond-shaped hierarchies which is a bit sad.

[david-christiansen]

You can avoid the diamond problem like this:

interface VerifiedFunctor (f : Type -> Type) (dict : Functor f) where
  ...

interface VerifiedApplicative (f : Type -> Type) (df : Functor f) (vdf : VerifiedFunctor f df) (dict : Applicative f df) where
  ...

with one issue: Applicative would need to track equalities over dictionaries as well. It would be nice to have a way to specify which superclass instances were used (some kind of sharing constraint) so that we can get the necessary equalities.

[ahmadsalim]

@david-christiansen Thanks for the workaround!
Although it does seem somewhat inoptimal as you mentioned :)

[nicolabotta]

Is there any chance to get diamond shaped hierarchies working properly as a milestone for 1.0? I would not mind having to write

foo : (A t, B t) => ...

instead of simply

foo : (B t) => ...

in situations in which foo uses features of both A and B and when B is a refinement of A:

interface A t where ...
interface (A t) => B t where ...

This would anyway be cleaner and more consistent with the way module features are currently treated: as a default, one cannot access features of modules that have been imported by imported modules, can one?

But without support for diamond shaped hierarchies, I really do not see how interfaces
can be used in sizeable projects in a proficient way ... I might be missing something, of course.