data Gnu : Type where [noHints, uniqueSearch]  ||| Use Bool stop proof search from using constructors  G : Bool -> Gnu  N : Bool -> Gnu  U : Bool -> Gnu ||| Makes interaction a bit nicerShow Gnu where  show (G _) = "G"  show (N _) = "N"  show (U _) = "U"  FooG : GnuFooG = G True FooN : GnuFooN = N True FooU : GnuFooU = U True ||| Curried versionsCooG : Unit -> GnuCooG _ = FooG CooN : Unit -> GnuCooN _ = FooN  CooU : Unit -> GnuCooU _ = FooU ||| We'll use this to see what proof Idris finds.Guess : {auto gnu : Gnu} -> StringGuess {gnu} = show gnu ||| Calls `Guess {gnu = gnu}` as expectedTestOK1 : (gnu : Gnu) -> StringTestOK1 gnu = Guess ||| Calls `Guess {gnu = f ()}` as expectedTestOK2 : (f : Unit -> Gnu) -> StringTestOK2 f = Guess ||| This is the meat. I'd expect this function to raise an error||| because it is ambiguous which local/local function to use.TestSurprise1 : (gnu1, gnu2 : Gnu) -> StringTestSurprise1 gnu1 gnu2 = Guess TestSurprise2 : (f,g : Unit -> Gnu) -> StringTestSurprise2 f g = Guess TestSurprise3 : (Unit -> Gnu, Unit -> Gnu) -> StringTestSurprise3 f = Guess