Interactive proof that fails with a type error

Applicative.idr

module Verified.Applicative

%default total

class Applicative f => VerifiedApplicative (f : Type -> Type) where
  applicativeMap : (x : f a) -> (g : a -> b) ->
                   map g x = pure g <$> x
  applicativeIdentity : (x : f a) -> pure id <$> x = x
  applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
                           ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)
  applicativeHomomorphism : (x : a) -> (g : a -> b) ->
                            (<$>) {f} (pure g) (pure x) = pure {f} (g x)
  applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
                           g <$> pure x = pure (\g' : a -> b => g' x) <$> g

Either.idr

module Verified.Applicative.Either

import Verified.Applicative

instance VerifiedApplicative (Either a) where
  applicativeMap (Left _) _ = refl
  applicativeMap (Right _) _ = refl
  applicativeIdentity (Left _) = refl
  applicativeIdentity (Right _) = refl
  applicativeComposition x g1 (Left _) = refl
  applicativeComposition x (Left _) _ = ?lemma -- LOOK HERE!
  applicativeComposition x (Left _) (Right _) = refl
  applicativeComposition (Left x) (Right _) (Right _) = refl
  applicativeComposition (Right _) (Right _) (Right _) = refl
  applicativeHomomorphism x g = refl
  applicativeInterchange x (Left _) = refl
  applicativeInterchange x (Right _) = refl

Interaction

-Verified.Applicative.Either.lemma> intros
----------              Other goals:              ----------
{hole6},{hole5},{hole4},{hole3},{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 a : Type
 a1 : Type
 b : Type
 c : Type
 x : Either a a1
 _t : a
 g2 : Either a (b -> c)
----------                 Goal:                  ----------
{hole7} : Either e instance of Prelude.Applicative.Applicative, method <$> a
                                                                           (Either e instance of Prelude.Applicative.Applicative, method <$> a
                                                                                                                                             (Either e instance of Prelude.Applicative.Applicative, method <$> a
                                                                                                                                                                                                               (Right (.))
                                                                                                                                                                                                               g2)
                                                                                                                                             (Left _t))
                                                                           x =
          Either e instance of Prelude.Applicative.Applicative, method <$> a g2 (Left _t)
-Verified.Applicative.Either.lemma> exact refl 
lemma: No more goals.
-Verified.Applicative.Either.lemma> qed