Different behaviour when working across different modules

Hello. Let's say we have a first module:

module TestA where

import Prelude (Show)

data N where { O :: N; S :: N -> N }
  deriving (Show)

{-@ infixl 5 +. @-}   
{-@ reflect +. @-}
{-@ (+.) :: N -> N -> N @-}
(+.) = \m n -> case m of { O -> n; S k -> S (k +. n) }

and a second module importing previous one

module TestB where

import Language.Haskell.Liquid.Equational
import Prelude (Show)
import TestA

data List a where { E :: List a; C :: a -> List a -> List a }
  deriving (Show)

{-@ reflect length @-}
{-@ length :: List a -> N @-}
length :: List a -> N
length = \l -> case l of { E -> O; x`C`xs -> S (length xs) }

{-@ infixl 7 ++ @-}   
{-@ reflect ++ @-}
{-@ (++) :: List a -> List a -> List a @-}
(++) :: List a -> List a -> List a
(++) = \l1 l2 -> case l1 of { E -> l2; x`C`xs -> x `C` (xs ++ l2) }

{-@ lemma :: l1:List a -> l2:List a -> { length (l1 ++ l2) = (length l1) +. (length l2) } @-}
lemma :: List a -> List a -> Proof
-- proof here

I see the following parsing error concering the +. operator in the lemma declaration:

However, if i put all these definitions inside the same module, there is no problem. How come?