idris_3791_VerifiedField.idr

-- idris 1.0
-- idris --noprelude

module Main

infixl 7 <.>

Not : Type -> Type
Not a = a -> Void

interface I1 ty where

interface I1 ty => I2 ty where
  neutral : ty

interface I2 a => I5 a where
  (<.>) : a -> a -> a

interface I5 a => I6 a where
  unity : a

interface I6 a => I7 a where
  inverseM : (x : a) -> Not (x = Main.neutral) -> a

interface I1 a => VI1 a where

interface (VI1 a, I2 a) => VI2 a where

interface (VI2 a, I5 a) => VI5 a where

interface (VI5 a, I6 a) => VI6 a where

interface (VI6 a, I7 a) => VI7 a where
  total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = (Main.neutral))) -> l <.> (inverseM l notId) = Main.unity  

-- see https://github.com/idris-lang/Idris-dev/issues/3791

{- compile error:
t.idr:33:11:When checking type of Main.fieldInverseIsInverseL:
Can't find implementation for I6 bqty

Possible cause:
        t.idr:34:99:When checking an application of function Main.inverseM:
                Type mismatch between
                        Not (l =
                             neutral {{constructor of Main.VI2#I2 a {{constructo
r of Main.VI5#VI2 a {{constructor of Main.VI6#VI5 a {{constructor of Main.VI7#VI
6 a a


    _}}}}}}}}) (Type of notId)
                and
                        Not (l =
                             neutral {{constructor of Main.I5#I2 a {{constructor
 of Main.I6#I5 a {{constructor of Main.I7#I6 a {{constructor of Main.VI7#I7 a a

                                                                              _}
}}}}}}}) (Expected type)

                Specifically:
                        Type mismatch between
                                neutral {{constructor of Main.VI2#I2 a {{constru
ctor of Main.VI5#VI2 a {{constructor of Main.VI6#VI5 a {{constructor of Main.VI7
#VI6 a a


       _}}}}}}}}
                        and
                                neutral {{constructor of Main.I5#I2 a {{construc
tor of Main.I6#I5 a {{constructor of Main.I7#I6 a {{constructor of Main.VI7#I7 a
 a


 _}}}}}}}}
-}