content: {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE FlexibleInstances         #-}
  {-# LANGUAGE FlexibleContexts          #-}
  {-# LANGUAGE UndecidableInstances      #-}
  {-# LANGUAGE TupleSections             #-}
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE DeriveDataTypeable        #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  {-# LANGUAGE TemplateHaskellQuotes     #-}
  {-# OPTIONS_GHC -Wno-orphans           #-}
  
  module Language.Haskell.Liquid.Parse
    ( hsSpecificationP
    , parseSpecComments
    , singleSpecP
    , BPspec (..)
    , parseTest'
    )
    where
  
  import           Control.Arrow                          (second)
  import           Control.Monad
  import           Control.Monad.Identity
  import           Data.Bifunctor                         (first)
  import qualified Data.Char                              as Char
  import qualified Data.Foldable                          as F
  import           Data.String
  import           Data.Void
  import           Prelude                                hiding (error)
  import           Text.Megaparsec                        hiding (ParseError)
  import           Text.Megaparsec.Char
  import qualified Data.HashMap.Strict                    as M
  import qualified Data.HashSet                           as S
  import           Data.Data
  import qualified Data.Maybe                             as Mb -- (isNothing, fromMaybe)
  import           Data.Char                              (isSpace, isAlphaNum)
  import           Data.List                              (partition)
  import qualified Text.PrettyPrint.HughesPJ              as PJ
  import           Text.PrettyPrint.HughesPJ.Compat       ((<+>))
  import           Language.Fixpoint.Types                hiding (panic, SVar, DDecl, DataDecl, DataCtor (..), Error, R, Predicate)
  import           Language.Haskell.Liquid.GHC.Misc       hiding (getSourcePos)
  import           Language.Haskell.Liquid.Types.Bounds
  import           Language.Haskell.Liquid.Types.DataDecl
  import           Language.Haskell.Liquid.Types.Errors
  import           Language.Haskell.Liquid.Types.Names
  import           Language.Haskell.Liquid.Types.PredType
  import           Language.Haskell.Liquid.Types.RType
  import           Language.Haskell.Liquid.Types.RefType
  import           Language.Haskell.Liquid.Types.RTypeOp
  import           Language.Haskell.Liquid.Types.Specs
  import           Language.Haskell.Liquid.Types.Types
  import           Language.Haskell.Liquid.Types.Variance
  import qualified Language.Haskell.Liquid.Misc           as Misc
  import qualified Language.Haskell.Liquid.Measure        as Measure
  import           Language.Fixpoint.Parse                hiding (Parser, dataDeclP, refBindP, refP, refDefP, parseTest')
  import qualified Liquid.GHC.API                         as GHC
  
  import Control.Monad.State
  
  -- * Top-level parsing API
  
  hsSpecificationP :: GHC.ModuleName -> [BPspec] -> (ModName, BareSpecParsed)
  hsSpecificationP modName specs = (ModName SrcImport modName, mkSpec specs)
  
  -- | Parse comments in .hs and .lhs files
  parseSpecComments :: [(SourcePos, String)] -> Either [Error] [BPspec]
  parseSpecComments specComments =
    case go ([], []) initPStateWithList specComments of
      ([], specs) ->
        Right specs
      (errors, _) ->
        Left errors
    where
      go :: ([Error], [BPspec])   -- accumulated errors and parsed specs (in reverse order)
         -> LHPState              -- parser state (primarily infix operator priorities)
         -> [(SourcePos, String)] -- remaining unparsed spec comments
         -> ([Error], [BPspec])   -- final errors and parsed specs
      go (errors, specs) _ []
        = (reverse errors, reverse specs)
      go (errors, specs) pstate ((pos, specComment):xs)
        = -- 'specP' parses a single spec comment, i.e., a single LH directive
          -- we allow a "block" of specs now
          case parseWithError pstate (block specP) pos specComment of
            Left err'       -> go (parseErrorBundleToErrors err' ++ errors, specs) pstate xs
            Right (st,spec) -> go (errors,spec ++ specs) st xs
  
  type LHPState = PStateV LocSymbol
  type Parser = ParserV LocSymbol
  
  instance ParseableV LocSymbol where
    parseV = locSymbolP
    mkSu = Su . M.fromList . reverse . filter notTrivial
      where
        notTrivial (x, EVar y) = x /= val y
        notTrivial _           = True
    vFromString = fmap symbol
  
  initPStateWithList :: LHPState
  initPStateWithList
    = (initPState composeFun)
                 { empList    = Just $ \lx -> EVar (symbol (show '[]) <$ lx)
                 , singList   = Just (\lx e -> EApp (EApp (EVar (symbol (show '(:)) <$ lx)) e) (EVar (symbol (show '[]) <$ lx)))
                 }
    where composeFun = Nothing
  
  -------------------------------------------------------------------------------
  singleSpecP :: SourcePos -> String -> Either (ParseErrorBundle String Void) BPspec
  -------------------------------------------------------------------------------
  singleSpecP pos = mapRight snd . parseWithError initPStateWithList specP pos
  
  mapRight :: (a -> b) -> Either l a -> Either l b
  mapRight f (Right x) = Right $ f x
  mapRight _ (Left x)  = Left x
  
  -- Note [PState in parser]
  --
  -- In the original parsec parser, 'PState' did not contain the supply counter.
  -- The supply counter was separately initialised to 0 on every parser call, e.g.
  -- in 'parseWithError'.
  --
  -- Now, the supply counter is a part of 'PState' and would normally be threaded
  -- between subsequent parsing calls within s single file, as for example issued
  -- by 'hsSpecificationP'. This threading seems correct to me (Andres). It sounds
  -- like we would want to have the same behaviour of the counter whether we are
  -- parsing several separate specs or a single combined spec.
  --
  -- However, I am getting one test failure due to the threading change, namely
  -- Tests.Micro.class-laws-pos.FreeVar.hs, because in a unification call two
  -- variables occurring in a binding position do not match. This seems like a bug
  -- in the unifier. I'm nevertheless reproucing the "old" supply behaviour for
  -- now. This should be revisited later. TODO.
  
  -- | Entry point for parsers.
  --
  -- Resets the supply in the given state to 0, see Note [PState in parser].
  -- Also resets the layout stack, as different spec comments in a file can
  -- start at different columns, and we do not want layout info to carry
  -- across different such comments.
  --
  parseWithError :: forall a. LHPState -> Parser a -> SourcePos -> String -> Either (ParseErrorBundle String Void) (LHPState, a)
  parseWithError pstate parser p s =
    case snd (runIdentity (runParserT' (runStateT doParse pstate{supply = 0, layoutStack = Empty}) internalParserState)) of
      Left peb -> Left peb
      Right (r, st) -> Right (st, r)
    where
      doParse :: Parser a
      doParse = spaces *> parser <* eof
      internalParserState =
        State
          { stateInput = s
          , stateOffset = 0
          , statePosState =
            PosState
              { pstateInput = s
              , pstateOffset = 0
              , pstateSourcePos = p
              , pstateTabWidth = defaultTabWidth
              , pstateLinePrefix = ""
              }
          , stateParseErrors = []
          }
  
  -- | Function to test parsers interactively.
  parseTest' :: Show a => Parser a -> String -> IO ()
  parseTest' parser input =
    parseTest (evalStateT parser initPStateWithList) input
  
  parseErrorBundleToErrors :: ParseErrorBundle String Void -> [Error]
  parseErrorBundleToErrors (ParseErrorBundle errors posState) =
    let
      (es, _) = attachSourcePos errorOffset errors posState
    in
      parseErrorError <$> F.toList es
  
  ---------------------------------------------------------------------------
  parseErrorError     :: (ParseError, SourcePos) -> Error
  ---------------------------------------------------------------------------
  parseErrorError (e, pos) = ErrParse sp msg e
    where
      sp              = sourcePosSrcSpan pos
      msg             = "Error Parsing Specification from:" <+> PJ.text (sourceName pos)
  
  --------------------------------------------------------------------------------
  -- | BareTypes -----------------------------------------------------------------
  --------------------------------------------------------------------------------
  
  {- | [NOTE:BARETYPE-PARSE] Fundamentally, a type is of the form
  
        comp -> comp -> ... -> comp
  
  So
  
    bt = comp
       | comp '->' bt
  
    comp = circle
         | '(' bt ')'
  
    circle = the ground component of a baretype, sans parens or "->" at the top level
  
  Each 'comp' should have a variable to refer to it,
  either a parser-assigned one or given explicitly. e.g.
  
    xs : [Int]
  
  -}
  
  data ParamComp = PC { _pci :: PcScope
                      , _pct :: BareTypeParsed }
  
  data PcScope = PcImplicit Symbol
               | PcExplicit Symbol
               | PcNoSymbol
               deriving (Eq,Show)
  
  nullPC :: BareTypeParsed -> ParamComp
  nullPC bt = PC PcNoSymbol bt
  
  btP :: Parser ParamComp
  btP = do
    c@(PC sb _) <- compP
    case sb of
      PcNoSymbol   -> return c
      PcImplicit b -> parseFun c b
      PcExplicit b -> parseFun c b
    <?> "btP"
    where
      parseFun c@(PC sb t1) sy  =
        (do
              reservedOp "->"
              PC _ t2 <- btP
              return (PC sb (mkRFun sy t1 t2)))
          <|>
           (do
              reservedOp "=>"
              PC _ t2 <- btP
              -- TODO:AZ return an error if s == PcExplicit
              return $ PC sb $ foldr (mkRFun dummySymbol) t2 (getClasses t1))
           <|>
            (do
               b <- locInfixSymbolP
               PC _ t2 <- btP
               return $ PC sb $ RApp
                 (mkBTyCon $ fmap (makeUnresolvedLHName LHTcName) b)
                 [t1,t2]
                 []
                 trueURef
            )
           <|> return c
  
      mkRFun b t t' = RFun b defRFInfo t t' trueURef
  
  compP :: Parser ParamComp
  compP = circleP <|> parens btP <?> "compP"
  
  circleP :: Parser ParamComp
  circleP
    =  nullPC <$> (reserved "forall" >> bareAllP)
   <|> holePC                                 -- starts with '_'
   <|> namedCircleP                           -- starts with lower
   <|> bareTypeBracesP                        -- starts with '{'
   <|> unnamedCircleP
   <|> anglesCircleP                          -- starts with '<'
   <|> nullPC <$> dummyP bbaseP               -- starts with '_' or '[' or '(' or lower or "'" or upper
   <?> "circleP"
  
  anglesCircleP :: Parser ParamComp
  anglesCircleP
    = angles $ do
        PC sb t <- parens btP
        p       <- monoPredicateP
        return   $ PC sb (t `strengthenUReft` MkUReft trueReft p)
  
  holePC :: Parser ParamComp
  holePC = do
    h <- holeP
    b <- dummyBindP
    return (PC (PcImplicit b) h)
  
  namedCircleP :: Parser ParamComp
  namedCircleP = do
    lb <- locLowerIdP
    do _ <- reservedOp ":"
       let b = val lb
       PC (PcExplicit b) <$> bareArgP b
      <|> do
        b <- dummyBindP
        PC (PcImplicit b) <$> dummyP (lowerIdTail lb)
  
  unnamedCircleP :: Parser ParamComp
  unnamedCircleP = do
    lb <- located dummyBindP
    let b = val lb
    t1 <- bareArgP b
    return $ PC (PcImplicit b) t1
  
  -- ---------------------------------------------------------------------
  
  -- | The top-level parser for "bare" refinement types. If refinements are
  -- not supplied, then the default "top" refinement is used.
  
  bareTypeP :: Parser BareTypeParsed
  bareTypeP = do
    PC _ v <- btP
    return v
  
  bareTypeBracesP :: Parser ParamComp
  bareTypeBracesP = do
    t <-  try (braces (
              try (Right <$> constraintP)
             <|>
              (do
                      x  <- symbolP
                      _ <- reservedOp ":"
                      -- NOSUBST i  <- freshIntP
                      t  <- bbaseP
                      reservedOp "|"
                      ra <- refasHoleP
                      -- xi is a unique var based on the name in x.
                      -- su replaces any use of x in the balance of the expression with the unique val
                      -- NOSUBST let xi = intSymbol x i
                      -- NOSUBST let su v = if v == x then xi else v
                      return $ Left $ PC (PcExplicit x) $ t (Reft (x, ra)) )
              )) <|> try (helper holeOrPredsP) <|> helper predP
    case t of
      Left l -> return l
      Right ct -> do
        PC _sb tt <- btP
        return $ nullPC $ rrTy ct tt
    where
      holeOrPredsP
        = (reserved "_" >> return hole)
       <|> try (pAnd <$> brackets (sepBy predP semi))
      helper p = braces $ do
        t <- RHole . uTop . Reft . ("VV",) <$> p
        return (Left $ nullPC t)
  
  
  bareArgP :: Symbol -> Parser BareTypeParsed
  bareArgP vvv
    =  refDefP vvv refasHoleP bbaseP    -- starts with '{'
   <|> holeP                            -- starts with '_'
   <|> dummyP bbaseP
   <|> parens bareTypeP                 -- starts with '('
                                        -- starts with '_', '[', '(', lower, upper
   <?> "bareArgP"
  
  bareAtomP
    :: (Parser (ExprV LocSymbol) -> Parser (ReftV LocSymbol -> BareTypeParsed) -> Parser BareTypeParsed)
    -> Parser BareTypeParsed
  bareAtomP ref
    =  ref refasHoleP bbaseP
   <|> holeP
   <|> dummyP bbaseP
   <?> "bareAtomP"
  
  bareAtomBindP :: Parser BareTypeParsed
  bareAtomBindP = bareAtomP refBindBindP
  
  
  -- Either
  --  { x : t | ra }
  -- or
  --  { ra }
  refBindBindP :: Parser (ExprV LocSymbol)
               -> Parser (ReftV LocSymbol -> BareTypeParsed)
               -> Parser BareTypeParsed
  refBindBindP rp kindP'
    = braces (
        (do
                x  <- symbolP
                _ <- reservedOp ":"
                -- NOSUBST i  <- freshIntP
                t  <- kindP'
                reservedOp "|"
                ra <- rp
                -- xi is a unique var based on the name in x.
                -- su replaces any use of x in the balance of the expression with the unique val
                -- NOSUBST let xi = intSymbol x i
                -- NOSUBST let su v = if v == x then xi else v
                return $ {- substa su $ NOSUBST -} t (Reft (x, ra)) )
       <|> (RHole . uTop . Reft . ("VV",) <$> rp)
       <?> "refBindBindP"
     )
  
  
  refDefP :: Symbol
          -> Parser (ExprV LocSymbol)
          -> Parser (ReftV LocSymbol -> BareTypeParsed)
          -> Parser BareTypeParsed
  refDefP sy rp kindP' = braces $ do
    x       <- optBindP sy
    -- NOSUBST i       <- freshIntP
    t       <- try (kindP' <* reservedOp "|") <|> return (RHole . uTop) <?> "refDefP"
    ra      <- rp
    -- xi is a unique var based on the name in x.
    -- su replaces any use of x in the balance of the expression with the unique val
    -- NOSUBST let xi   = intSymbol x i
    -- NOSUBST let su v = if v == x then xi else v
    return   $ {- substa su $ NOSUBST -} t (Reft (x, ra))
         -- substa su . t . Reft . (x,) <$> (rp <* spaces))
        --  <|> ((RHole . uTop . Reft . ("VV",)) <$> (rp <* spaces))
  
  refP :: Parser (ReftV LocSymbol -> BareTypeParsed) -> Parser BareTypeParsed
  refP = refBindBindP refaP
  
  relrefaP :: Parser (RelExprV LocSymbol)
  relrefaP =
    try (ERUnChecked <$> refaP <* reserved ":=>" <*> relrefaP)
      <|> try (ERChecked <$> refaP <* reserved "!=>" <*> relrefaP)
      <|> ERBasic <$> refaP
  
  -- "sym :" or return the devault sym
  optBindP :: Symbol -> Parser Symbol
  optBindP x = try bindP <|> return x
  
  holeP :: Parser BareTypeParsed
  holeP    = reserved "_" >> return (RHole $ uTop $ Reft ("VV", hole))
  
  holeRefP :: Parser (ReftV v -> BareTypeV v)
  holeRefP = reserved "_" >> return (RHole . uTop)
  
  -- NOPROP refasHoleP :: Parser Expr
  -- NOPROP refasHoleP  = try refaP
  -- NOPROP          <|> (reserved "_" >> return hole)
  
  refasHoleP :: Parser (ExprV LocSymbol)
  refasHoleP
    =  (reserved "_" >> return hole)
   <|> refaP
   <?> "refasHoleP"
  
  bbaseP :: Parser (ReftV LocSymbol -> BareTypeParsed)
  bbaseP
    =  holeRefP  -- Starts with '_'
   <|> liftM2 bLst (brackets (optional bareTypeP)) predicatesP
   <|> liftM2 bTup (parens $ sepBy (maybeBind bareTypeP) comma) predicatesP
   <|> try parseHelper  -- starts with lower
   <|> liftM4 bCon bTyConP predicatesP (many bareTyArgP) mmonoPredicateP
             -- starts with "'" or upper case char
   <?> "bbaseP"
   where
     parseHelper = do
       l <- located lowerIdP
       lowerIdTail l
  
  maybeBind :: Parser a -> Parser (Maybe Symbol, a)
  maybeBind parser = do {bd <- maybeP' bbindP; ty <- parser ; return (bd, ty)}
    where
      maybeP' p = try (Just <$> p)
               <|> return Nothing
  
  lowerIdTail :: LocSymbol -> Parser (ReftV LocSymbol -> BareTypeParsed)
  lowerIdTail l =
            fmap (bAppTy (bTyVar l)) (some bareTyArgP)
        <|> fmap (bRVar (bTyVar l)) monoPredicateP
  
  bTyConP :: Parser BTyCon
  bTyConP
    =  (reservedOp "'" >> mkPromotedBTyCon <$> locUpperIdLHNameP (LHDataConName LHAnyModuleNameF))
   <|> mkBTyCon <$> locUpperIdLHNameP LHTcName
   <|> (reserved "*" >>
          return (mkBTyCon (dummyLoc $ makeUnresolvedLHName LHTcName $ symbol ("*" :: String)))
       )
   <?> "bTyConP"
  
  locUpperIdLHNameP :: LHNameSpace -> Parser (Located LHName)
  locUpperIdLHNameP ns = fmap (makeUnresolvedLHName ns) <$> locUpperIdP
  
  mkPromotedBTyCon :: Located LHName -> BTyCon
  mkPromotedBTyCon x = BTyCon x False True -- (consSym '\'' <$> x) False True
  
  classBTyConP :: Parser BTyCon
  classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP LHTcName
  
  mkClassBTyCon :: Located LHName -> BTyCon
  mkClassBTyCon x = BTyCon x True False
  
  bbaseNoAppP :: Parser (ReftV LocSymbol -> BareTypeParsed)
  bbaseNoAppP
    =  holeRefP
   <|> liftM2 bLst (brackets (optional bareTypeP)) predicatesP
   <|> liftM2 bTup (parens $ sepBy (maybeBind bareTypeP) comma) predicatesP
   <|> try (liftM4 bCon bTyConP predicatesP (return []) (return $ Pr []))
   <|> liftM2 bRVar (bTyVar <$> located lowerIdP) monoPredicateP
   <?> "bbaseNoAppP"
  
  bareTyArgP :: Parser BareTypeParsed
  bareTyArgP
    =  (RExprArg . fmap (ECon . I) <$> locNatural)
   <|> try (braces $ RExprArg <$> located exprP)
   <|> try bareAtomNoAppP
   <|> try (parens bareTypeP)
   <?> "bareTyArgP"
  
  bareAtomNoAppP :: Parser BareTypeParsed
  bareAtomNoAppP
    =  refP bbaseNoAppP
   <|> dummyP bbaseNoAppP
   <?> "bareAtomNoAppP"
  
  
  constraintP :: Parser BareTypeParsed
  constraintP
    = do xts <- constraintEnvP
         t1  <- bareTypeP
         reservedOp "<:"
         fromRTypeRep . RTypeRep [] []
                                 ((val . fst <$> xts) ++ [dummySymbol])
                                 (replicate (length xts + 1) defRFInfo)
                                 (replicate (length xts + 1) trueURef)
                                 ((snd <$> xts) ++ [t1]) <$> bareTypeP
  
  trueURef :: UReftV v (ReftV v)
  trueURef = MkUReft trueReft (Pr [])
  
  constraintEnvP :: Parser [(LocSymbol, BareTypeParsed)]
  constraintEnvP
     =  try (do xts <- sepBy tyBindNoLocP comma
                reservedOp "|-"
                return xts)
    <|> return []
    <?> "constraintEnvP"
  
  rrTy :: BareTypeParsed -> BareTypeParsed -> BareTypeParsed
  rrTy ct = RRTy (xts ++ [(dummySymbol, tr)]) trueURef OCons
    where
      tr   = ty_res trep
      xts  = zip (ty_binds trep) (ty_args trep)
      trep = toRTypeRep ct
  
  --  "forall <z w> . TYPE"
  -- or
  --  "forall x y <z :: Nat, w :: Int> . TYPE"
  bareAllP :: Parser BareTypeParsed
  bareAllP = do
    sp <- getSourcePos
    as  <- tyVarDefsP
    ps  <- angles inAngles
          <|> return []
    _ <- dot
    t <- bareTypeP
    return $ foldr rAllT (foldr (rAllP sp) t ps) (makeRTVar <$> as)
    where
      rAllT a t = RAllT a t trueURef
      inAngles  = try  (sepBy  predVarDefP comma)
  
  -- See #1907 for why we have to alpha-rename pvar binders
  rAllP :: SourcePos -> PVarV LocSymbol (BSortV LocSymbol) -> BareTypeParsed -> BareTypeParsed
  rAllP sp p t = RAllP p' ({- F.tracepp "rAllP" $ -} substPVar p p' t)
    where
      p'  = p { pname = pn' }
      pn' = pname p `intSymbol` lin `intSymbol` col
      lin = unPos (sourceLine sp)
      col = unPos (sourceColumn  sp)
  
  tyVarDefsP :: Parser [BTyVar]
  tyVarDefsP
    = parens (many (bTyVar <$> located tyKindVarIdP))
   <|> many (bTyVar <$> located tyVarIdP)
   <?> "tyVarDefsP"
  
  tyKindVarIdP :: Parser Symbol
  tyKindVarIdP = do
     tv <- tyVarIdP
     do reservedOp "::"; _ <- kindP; return tv <|> return tv
  
  kindP :: Parser BareTypeParsed
  kindP = bareAtomBindP
  
  predVarDefsP :: Parser [PVarV LocSymbol (BSortV LocSymbol)]
  predVarDefsP
    =  angles (sepBy1 predVarDefP comma)
   <|> return []
   <?> "predVarDefP"
  
  predVarDefP :: Parser (PVarV LocSymbol (BSortV LocSymbol))
  predVarDefP
    = bPVar <$> predVarIdP <*> reservedOp "::" <*> propositionSortP
  
  predVarIdP :: Parser Symbol
  predVarIdP
    = symbol <$> tyVarIdP
  
  bPVar :: Symbol -> t -> [(Symbol, t1)] -> PVarV LocSymbol t1
  bPVar p _ xts  = PV p τ dummySymbol τxs
    where
      (_, τ) = safeLast "bPVar last" xts
      τxs    = [ (τ', x, EVar (dummyLoc x)) | (x, τ') <- init xts ]
      safeLast _ xs@(_:_) = last xs
      safeLast msg _      = panic Nothing $ "safeLast with empty list " ++ msg
  
  propositionSortP :: Parser [(Symbol, BSortV LocSymbol)]
  propositionSortP = map (fmap toRSort) <$> propositionTypeP
  
  propositionTypeP :: Parser [(Symbol, BareTypeParsed)]
  propositionTypeP = either fail return . mkPropositionType =<< bareTypeP
  
  mkPropositionType :: BareTypeParsed -> Either String [(Symbol, BareTypeParsed)]
  mkPropositionType t
    | isOk      = Right $ zip (ty_binds tRep) (ty_args tRep)
    | otherwise = Left mkErr
    where
      isOk      = isPropBareType (ty_res tRep)
      tRep      = toRTypeRep t
      mkErr     = "Proposition type with non-Bool output: " ++ showpp (parsedToBareType t)
  
  xyP :: Parser x -> Parser a -> Parser y -> Parser (x, y)
  xyP lP sepP rP =
    (,) <$> lP <* sepP <*> rP
  
  dummyBindP :: Parser Symbol
  dummyBindP = tempSymbol "db" <$> freshIntP
  
  isPropBareType :: RTypeV v BTyCon t t1 -> Bool
  isPropBareType (RApp tc [] _ _) =
      case val (btc_tc tc) of
        LHNUnresolved _ s -> s == boolConName
        _ -> False
  isPropBareType _ = False
  
  getClasses :: RTypeV v BTyCon t t1 -> [RTypeV v BTyCon t t1]
  getClasses (RApp tc ts ps r)
    | isTuple tc
    = concatMap getClasses ts
    | otherwise
    = [RApp (tc { btc_class = True }) ts ps r]
  getClasses t
    = [t]
  
  dummyP ::  Monad m => m (ReftV LocSymbol -> b) -> m b
  dummyP fm
    = fm `ap` return trueReft
  
  symsP :: Monoid r
        => Parser [(Symbol, RTypeV v c BTyVar r)]
  symsP
    = do reservedOp "\\"
         ss <- many symbolP
         reservedOp "->"
         return $ (, dummyRSort) <$> ss
   <|> return []
   <?> "symsP"
  
  dummyRSort :: Monoid r => RTypeV v c BTyVar r
  dummyRSort
    = RVar (BTV "dummy") mempty
  
  predicatesP :: Monoid r
              => Parser [Ref (RTypeV LocSymbol c BTyVar r) BareTypeParsed]
  predicatesP
     =  angles (sepBy1 predicate1P comma)
    <|> return []
    <?> "predicatesP"
  
  predicate1P :: Monoid r
              => Parser (Ref (RTypeV LocSymbol c BTyVar r) BareTypeParsed)
  predicate1P
     =  try (RProp <$> symsP <*> refP bbaseP)
    <|> (rPropP [] . predUReft <$> monoPredicate1P)
    <|> braces (bRProp <$> symsP' <*> refaP)
    <?> "predicate1P"
     where
      symsP'       = do ss    <- symsP
                        fs    <- mapM refreshSym (fst <$> ss)
                        return $ zip ss fs
      refreshSym s = intSymbol s <$> freshIntP
  
  mmonoPredicateP :: Parser (PredicateV LocSymbol)
  mmonoPredicateP
     = try (angles $ angles monoPredicate1P)
    <|> return (Pr [])
    <?> "mmonoPredicateP"
  
  monoPredicateP :: Parser (PredicateV LocSymbol)
  monoPredicateP
     = try (angles monoPredicate1P)
    <|> return (Pr [])
    <?> "monoPredicateP"
  
  monoPredicate1P :: Parser (PredicateV LocSymbol)
  monoPredicate1P
     =  (reserved "True" >> return (Pr []))
    <|> (pdVar <$> parens predVarUseP)
    <|> (pdVar <$>        predVarUseP)
    <?> "monoPredicate1P"
  
  predVarUseP :: Parser (PVarV LocSymbol String)
  predVarUseP
    = do (p, xs) <- funArgsP
         return   $ PV p dummyTyId dummySymbol [ (dummyTyId, dummySymbol, x) | x <- xs ]
  
  funArgsP :: Parser (Symbol, [ExprV LocSymbol])
  funArgsP  = try realP <|> empP <?> "funArgsP"
    where
      empP  = (,[]) <$> predVarIdP
      realP = do (EVar lp, xs) <- splitEApp <$> funAppP
                 return (val lp, xs)
  
  boundP :: Parser (Bound (Located BareTypeParsed) (ExprV LocSymbol))
  boundP = do
    name   <- locUpperIdP
    reservedOp "="
    vs      <- bvsP
    params' <- many (parens tyBindP)
    args    <- bargsP
    Bound name vs params' args <$> predP
   where
      bargsP =     ( do reservedOp "\\"
                        xs <- many (parens tyBindP)
                        reservedOp  "->"
                        return xs
                   )
             <|> return []
             <?> "bargsP"
      bvsP   =     ( do reserved "forall"
                        xs <- many $ do
                          ls <- locSymbolP
                          pure $ bTyVar ls <$ ls
                        reservedOp  "."
                        return (fmap (`RVar` trueURef) <$> xs)
                   )
             <|> return []
  
  
  infixGenP :: Assoc -> Parser ()
  infixGenP assoc = do
     p <- maybeDigit
     s <- infixIdP -- TODO: Andres: infixIdP was defined as many (satisfy (`notElem` [' ', '.'])) which does not make sense at all
     -- Andres: going via Symbol seems unnecessary and wasteful here
     addOperatorP (FInfix p (symbolString s) Nothing assoc)
  
  infixP :: Parser ()
  infixP = infixGenP AssocLeft
  
  infixlP :: Parser ()
  infixlP = infixGenP AssocLeft
  
  infixrP :: Parser ()
  infixrP = infixGenP AssocRight
  
  maybeDigit :: Parser (Maybe Int)
  maybeDigit
    = optional (lexeme (read . pure <$> digitChar))
  
  ------------------------------------------------------------------------
  ----------------------- Wrapped Constructors ---------------------------
  ------------------------------------------------------------------------
  
  bRProp :: [((Symbol, τ), Symbol)]
         -> ExprV LocSymbol -> Ref τ (RTypeV LocSymbol c BTyVar (UReftV LocSymbol (ReftV LocSymbol)))
  bRProp []    _    = panic Nothing "Parse.bRProp empty list"
  bRProp syms' epr  = RProp ss $ bRVar (BTV $ dummyLoc dummyName) (Pr []) r
    where
      (ss, (v, _))  = (init symsf, last symsf)
      symsf         = [(y, s) | ((_, s), y) <- syms']
      su            = mkSubstLocSymbol [(x, EVar $ dummyLoc y) | ((x, _), y) <- syms', x /= v]
      r             = Reft (v, substExprV val su epr)
  
  mkSubstLocSymbol :: [(Symbol, ExprV LocSymbol)] -> SubstV LocSymbol
  mkSubstLocSymbol = Su . M.fromList . reverse . filter notTrivial
    where
      notTrivial (x, EVar y) = x /= val y
      notTrivial _           = True
  
  bRVar :: tv -> PredicateV v -> r -> RTypeV v c tv (UReftV v r)
  bRVar α p r = RVar α (MkUReft r p)
  
  bLst :: Maybe (RTypeV v BTyCon tv (UReftV v r))
       -> [RTPropV v BTyCon tv (UReftV v r)]
       -> r
       -> RTypeV v BTyCon tv (UReftV v r)
  bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [t] rs (reftUReft r)
  bLst Nothing  rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) []  rs (reftUReft r)
  
  bTup :: [(Maybe Symbol, BareTypeParsed)]
       -> [RTPropV LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))]
       -> ReftV LocSymbol
       -> BareTypeParsed
  bTup [(_,t)] _ r
    | isTauto (fmap val r)  = t
    | otherwise  = t `strengthenUReft` reftUReft r
  bTup ts rs r
    | all (Mb.isNothing . fst) ts || length ts < 2
    = RApp
        (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts))
        (snd <$> ts) rs (reftUReft r)
    | otherwise
    = RApp
        (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts))
        (mapReft (const trueURef) . snd <$> ts)
        rs'
        (reftUReft r)
    where
      args       = [(Mb.fromMaybe dummySymbol x, mapReft mempty t) | (x,t) <- ts]
      makeProp i = RProp (reverse $ take i args) ((snd <$> ts)!!i)
      rs'        = makeProp <$> [1..(length ts-1)]
  
  
  -- Temporarily restore this hack benchmarks/esop2013-submission/Array.hs fails
  -- w/o it
  -- TODO RApp Int [] [p] true should be syntactically different than RApp Int [] [] p
  -- bCon b s [RProp _ (RHole r1)] [] _ r = RApp b [] [] $ r1 `meet` (MkUReft r mempty s)
  bCon :: c
       -> [RTPropV v c tv (UReftV v r)]
       -> [RTypeV v c tv (UReftV v r)]
       -> PredicateV v
       -> r
       -> RTypeV v c tv (UReftV v r)
  bCon b rs ts p r = RApp b ts rs $ MkUReft r p
  
  bAppTy :: Foldable t => BTyVar -> t BareTypeParsed -> ReftV LocSymbol -> BareTypeParsed
  bAppTy v ts r  = strengthenUReft ts' (reftUReft r)
    where
      ts'        = foldl' (\a b -> RAppTy a b (uTop trueReft)) (RVar v (uTop trueReft)) ts
  
  strengthenUReft
    :: BareTypeParsed -> UReftV LocSymbol (ReftV LocSymbol) -> BareTypeParsed
  strengthenUReft = strengthenWith meetUReft
    where
      meetUReft (MkUReft r0 (Pr p0)) (MkUReft r1 (Pr p1)) =
         MkUReft (meetReftV r0 r1) (Pr $ p0 <> p1)
  
      meetReftV :: ReftV LocSymbol -> ReftV LocSymbol -> ReftV LocSymbol
      meetReftV (Reft (v, ra)) (Reft (v', ra'))
        | v == v'          = Reft (v , pAnd [ra, ra'])
        | v == dummySymbol = Reft (v', pAnd [ra', substExprV val (Su $ M.fromList [(v , EVar (dummyLoc v'))]) ra])
        | otherwise        = Reft (v , pAnd [ra, substExprV val (Su $ M.fromList [(v', EVar (dummyLoc v))]) ra'])
  
  substExprV :: (v -> Symbol) -> SubstV v -> ExprV v -> ExprV v
  substExprV toSym su0 = go
    where
      go (EApp f e) = EApp (go f) (go e)
      go (ELam x e) = ELam x (substExprV toSym (removeSubst su0 (fst x)) e)
      go (ECoerc a t e) = ECoerc a t (go e)
      go (ENeg e) = ENeg (go e)
      go (EBin op e1 e2) = EBin op (go e1) (go e2)
      go (EIte p e1 e2) = EIte (go p) (go e1) (go e2)
      go (ECst e so) = ECst (go e) so
      go (EVar x) = appSubst su0 x
      go (PAnd ps) = PAnd $ map go ps
      go (POr  ps) = POr $ map go ps
      go (PNot p) = PNot (go p)
      go (PImp p1 p2) = PImp (go p1) (go p2)
      go (PIff p1 p2) = PIff (go p1) (go p2)
      go (PAtom r e1 e2) = PAtom r (go e1) (go e2)
      go (PKVar k su') = PKVar k $ su' `appendSubst` su0
      go (PGrad k su' i e) = PGrad k (su' `appendSubst` su0) i (go e)
      go (PAll _ _) = panic Nothing "substExprV: PAll"
      go (PExist _ _) = panic Nothing "substExprV: PExist"
      go p = p
  
      appSubst (Su s) x = Mb.fromMaybe (EVar x) (M.lookup (toSym x) s)
  
      removeSubst (Su su) x = Su $ M.delete x su
  
      appendSubst (Su s1) θ2@(Su s2) = Su $ M.union s1' s2
        where
          s1' = substExprV toSym θ2 <$> s1
  
  
  reftUReft :: r -> UReftV v r
  reftUReft r    = MkUReft r (Pr [])
  
  predUReft :: PredicateV v -> UReftV v (ReftV v)
  predUReft = MkUReft trueReft
  
  dummyTyId :: String
  dummyTyId = ""
  
  ------------------------------------------------------------------
  --------------------------- Measures -----------------------------
  ------------------------------------------------------------------
  
  -- | The AST for a single parsed spec.
  data BPspec
    = Meas    (MeasureV LocSymbol LocBareTypeParsed (Located LHName)) -- ^ 'measure' definition
    | Assm    (Located LHName, LocBareTypeParsed)              -- ^ 'assume' signature (unchecked)
    | AssmReflect (Located LHName, Located LHName)             -- ^ 'assume reflects' signature (unchecked)
    | Asrt    (Located LHName, LocBareTypeParsed)              -- ^ 'assert' signature (checked)
    | Asrts   ([Located LHName], (LocBareTypeParsed, Maybe [Located (ExprV LocSymbol)])) -- ^ sym0, ..., symn :: ty / [m0,..., mn]
    | DDecl   DataDeclParsed                                -- ^ refined 'data'    declaration
    | NTDecl  DataDeclParsed                                -- ^ refined 'newtype' declaration
    | Relational (Located LHName, Located LHName, LocBareTypeParsed, LocBareTypeParsed, RelExprV LocSymbol, RelExprV LocSymbol) -- ^ relational signature
    | AssmRel (Located LHName, Located LHName, LocBareTypeParsed, LocBareTypeParsed, RelExprV LocSymbol, RelExprV LocSymbol) -- ^ 'assume' relational signature
    | Class   (RClass LocBareTypeParsed)                    -- ^ refined 'class' definition
    | RInst   (RInstance LocBareTypeParsed)                 -- ^ refined 'instance' definition
    | Invt    LocBareTypeParsed                             -- ^ 'invariant' specification
    | Using  (LocBareTypeParsed, LocBareTypeParsed)         -- ^ 'using' declaration (for local invariants on a type)
    | Alias   (RTAlias Symbol BareTypeParsed)                 -- ^ 'type' alias declaration
    | EAlias  (RTAlias Symbol (ExprV LocSymbol))  -- ^ 'predicate' alias declaration
    | Embed   (Located LHName, FTycon, TCArgs)              -- ^ 'embed' declaration
    | Qualif  (QualifierV LocSymbol)                        -- ^ 'qualif' definition
    | LVars   (Located LHName)                              -- ^ 'lazyvar' annotation, defer checks to *use* sites
    | Lazy    (Located LHName)                              -- ^ 'lazy' annotation, skip termination check on binder
    | Fail    (Located LHName)                              -- ^ 'fail' annotation, the binder should be unsafe
    | Rewrite (Located LHName)                              -- ^ 'rewrite' annotation, the binder generates a rewrite rule
    | Rewritewith (Located LHName, [Located LHName])        -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list,
    | Insts   (Located LHName)                              -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
    | HMeas   (Located LHName)                              -- ^ 'measure' annotation; lift Haskell binder as measure
    | Reflect (Located LHName)                              -- ^ 'reflect' annotation; reflect Haskell binder as function in logic
    | PrivateReflect LocSymbol                              -- ^ 'private-reflect' annotation
    | OpaqueReflect (Located LHName)                        -- ^ 'opaque-reflect' annotation
    | Inline  (Located LHName)                              -- ^ 'inline' annotation;  inline (non-recursive) binder as an alias
    | Ignore  (Located LHName)                              -- ^ 'ignore' annotation; skip all checks inside this binder
    | ASize   (Located LHName)                              -- ^ 'autosize' annotation; automatically generate size metric for this type
    | PBound  (Bound LocBareTypeParsed (ExprV LocSymbol))   -- ^ 'bound' definition
    | Pragma  (Located String)                              -- ^ 'LIQUID' pragma, used to save configuration options in source files
    | CMeas   (MeasureV LocSymbol LocBareTypeParsed ())     -- ^ 'class measure' definition
    | IMeas   (MeasureV LocSymbol LocBareTypeParsed (Located LHName)) -- ^ 'instance measure' definition
    | Varia   (Located LHName, [Variance])                  -- ^ 'variance' annotations, marking type constructor params as co-, contra-, or in-variant
    | DSize   ([LocBareTypeParsed], LocSymbol)              -- ^ 'data size' annotations, generating fancy termination metric
    | BFix    ()                                            -- ^ fixity annotation
    | Define  (Located LHName, ([Symbol], ExprV LocSymbol)) -- ^ 'define' annotation for specifying logic aliases
    deriving (Data)
  
  instance PPrint BPspec where
    pprintTidy = ppPspec
  
  splice :: PJ.Doc -> [PJ.Doc] -> PJ.Doc
  splice sep = PJ.hcat . PJ.punctuate sep
  
  ppAsserts :: (PPrint t) => Tidy -> [Located LHName] -> t -> Maybe [Located (ExprV LocSymbol)] -> PJ.Doc
  ppAsserts k lxs t mles
    = PJ.hcat [ splice ", " (map (pprintTidy k . val) lxs)
              , " :: "
              , pprintTidy k t
              , ppLes mles
              ]
    where
      ppLes Nothing    = ""
      ppLes (Just les) = "/" <+> pprintTidy k (fmap val . val <$> les)
  
  pprintSymbolWithParens :: LHName -> PJ.Doc
  pprintSymbolWithParens lhname =
      case symbolString $ getLHNameSymbol lhname of
        n@(c:_) | not (Char.isAlpha c) -> "(" <> PJ.text n <> ")"
        n -> PJ.text n
  
  ppPspec :: Tidy -> BPspec -> PJ.Doc
  ppPspec k (Meas m)
    = "measure" <+> pprintTidy k (val <$> unLocMeasureV m)
  ppPspec k (Assm (lx, t))
    = "assume"  <+> pprintSymbolWithParens (val lx) <+> "::" <+> pprintTidy k (parsedToBareType <$> t)
  ppPspec k (AssmReflect (lx, ly))
    = "assume reflect"  <+> pprintTidy k (val lx) <+> "as" <+> pprintTidy k (val ly)
  ppPspec k (Asrt (lx, t))
    = "assert"  <+> pprintTidy k (val lx) <+> "::" <+> pprintTidy k (parsedToBareType <$> t)
  ppPspec k (Asrts (lxs, (t, les)))
    = ppAsserts k lxs (parsedToBareType <$> t) les
  ppPspec k (DDecl d)
    = pprintTidy k (parsedToBareType <$> mapDataDeclV val d)
  ppPspec k (NTDecl d)
    = "newtype" <+> pprintTidy k (parsedToBareType <$> mapDataDeclV val d)
  ppPspec k (Invt t)
    = "invariant" <+> pprintTidy k (parsedToBareType <$> t)
  ppPspec k (Using (t1, t2))
    = "using" <+> pprintTidy k (parsedToBareType <$> t1) <+> "as" <+> pprintTidy k (parsedToBareType <$> t2)
  ppPspec k (Alias rta)
    = "type" <+> pprintTidy k (fmap parsedToBareType rta)
  ppPspec k (EAlias rte)
    = "predicate" <+> pprintTidy k rte
  ppPspec k (Embed   (lx, tc, NoArgs))
    = "embed" <+> pprintTidy k (val lx)         <+> "as" <+> pprintTidy k tc
  ppPspec k (Embed   (lx, tc, WithArgs))
    = "embed" <+> pprintTidy k (val lx) <+> "*" <+> "as" <+> pprintTidy k tc
  ppPspec k (Qualif  q)
    = pprintTidy k q
  ppPspec k (LVars   lx)
    = "lazyvar" <+> pprintTidy k (val lx)
  ppPspec k (Lazy   lx)
    = "lazy" <+> pprintTidy k (val lx)
  ppPspec k (Rewrite   lx)
    = "rewrite" <+> pprintTidy k (val lx)
  ppPspec k (Rewritewith (lx, lxs))
    = "rewriteWith" <+> pprintTidy k (val lx) <+> PJ.hsep (map go lxs)
    where
      go s = pprintTidy k $ val s
  ppPspec k (Fail   lx)
    = "fail" <+> pprintTidy k (val lx)
  ppPspec k (Insts   lx)
    = "automatic-instances" <+> pprintTidy k (val lx)
  ppPspec k (HMeas   lx)
    = "measure" <+> pprintTidy k (val lx)
  ppPspec k (Reflect lx)
    = "reflect" <+> pprintTidy k (val lx)
  ppPspec k (PrivateReflect lx)
    = "private-reflect" <+> pprintTidy k (val lx)
  ppPspec k (OpaqueReflect lx)
    = "opaque-reflect" <+> pprintTidy k (val lx)
  ppPspec k (Inline  lx)
    = "inline" <+> pprintTidy k (val lx)
  ppPspec k (Ignore  lx)
    = "ignore" <+> pprintTidy k (val lx)
  ppPspec k (ASize   lx)
    = "autosize" <+> pprintTidy k (val lx)
  ppPspec k (PBound  bnd)
    = pprintTidy k $ mapBoundTy (fmap parsedToBareType) bnd
  ppPspec _ (Pragma  (Loc _ _ s))
    = "LIQUID" <+> PJ.text s
  ppPspec k (CMeas   m)
    = "class measure" <+> pprintTidy k (unLocMeasureV m)
  ppPspec k (IMeas   m)
    = "instance measure" <+> pprintTidy k (val <$> unLocMeasureV m)
  ppPspec k (Class   cls)
    = pprintTidy k $ fmap (fmap parsedToBareType) cls
  ppPspec k (RInst   inst)
    = pprintTidy k $ fmap (fmap parsedToBareType) inst
  ppPspec k (Varia   (lx, vs))
    = "data variance" <+> pprintTidy k (val lx) <+> splice " " (pprintTidy k <$> vs)
  ppPspec k (DSize   (ds, ss))
    = "data size" <+> splice " " (pprintTidy k <$> map (fmap parsedToBareType) ds) <+> pprintTidy k (val ss)
  ppPspec _ (BFix    _)           --
    = "fixity"
  ppPspec k (Define  (lx, (ys, e)))
    = "define" <+> pprintTidy k (val lx) <+> " " <+> pprintTidy k ys <+> "=" <+> pprintTidy k e
  ppPspec k (Relational (lxl, lxr, tl, tr, q, p))
    = "relational"
          <+> pprintTidy k (val lxl) <+> "::" <+> pprintTidy k (parsedToBareType <$> tl) <+> "~"
          <+> pprintTidy k (val lxr) <+> "::" <+> pprintTidy k (parsedToBareType <$> tr) <+> "|"
          <+> pprintTidy k (fmap val q) <+> "=>" <+> pprintTidy k (fmap val p)
  ppPspec k (AssmRel (lxl, lxr, tl, tr, q, p))
    = "assume relational"
          <+> pprintTidy k (val lxl) <+> "::" <+> pprintTidy k (parsedToBareType <$> tl) <+> "~"
          <+> pprintTidy k (val lxr) <+> "::" <+> pprintTidy k (parsedToBareType <$> tr) <+> "|"
          <+> pprintTidy k (fmap val q) <+> "=>" <+> pprintTidy k (fmap val p)
  
  unLocMeasureV :: MeasureV LocSymbol LocBareTypeParsed v -> MeasureV Symbol LocBareType v
  unLocMeasureV = mapMeasureV val . mapMeasureTy (fmap parsedToBareType)
  
  -- | For debugging
  {-instance Show (Pspec a b) where
    show (Meas   _) = "Meas"
    show (Assm   _) = "Assm"
    show (Asrt   _) = "Asrt"
    show (Asrts  _) = "Asrts"
    show (Impt   _) = "Impt"
    shcl  _) = "DDecl"
    show (NTDecl _) = "NTDecl"
    show (Invt   _) = "Invt"
    show (Using _) = "Using"
    show (Alias  _) = "Alias"
    show (EAlias _) = "EAlias"
    show (Embed  _) = "Embed"
    show (Qualif _) = "Qualif"
    show (Decr   _) = "Decr"
    show (LVars  _) = "LVars"
    show (Lazy   _) = "Lazy"
    -- show (Axiom  _) = "Axiom"
    show (Reflect _) = "Reflect"
    show (HMeas  _) = "HMeas"
    show (Inline _) = "Inline"
    show (Pragma _) = "Pragma"
    show (CMeas  _) = "CMeas"
    show (IMeas  _) = "IMeas"
    show (Class  _) = "Class"
    show (Varia  _) = "Varia"
    show (PBound _) = "Bound"
    show (RInst  _) = "RInst"
    show (ASize  _) = "ASize"
    show (BFix   _) = "BFix"
    show (Define _) = "Define"-}
  
  -- | Turns a list of parsed specifications into a "bare spec".
  --
  -- This is primarily a rearrangement, as the bare spec is a record containing
  -- different kinds of spec directives in different positions, whereas the input
  -- list is a mixed list.
  --
  -- In addition, the sigs of the spec (these are asserted/checked LH type
  -- signatues) are being qualified, i.e., the binding occurrences are prefixed
  -- with the module name.
  --
  mkSpec :: [BPspec] -> Measure.Spec LocSymbol BareTypeParsed
  mkSpec xs = Measure.Spec
    { Measure.measures   = [m | Meas   m <- xs]
    , Measure.asmSigs    = [a | Assm   a <- xs]
    , Measure.asmReflectSigs = [(l, r) | AssmReflect (l, r) <- xs]
    , Measure.sigs       = [a | Asrt   a <- xs]
                        ++ [(y, t) | Asrts (ys, (t, _)) <- xs, y <- ys]
    , Measure.expSigs    = []
    , Measure.invariants = [(Nothing, t) | Invt   t <- xs]
    , Measure.ialiases   = [t | Using t <- xs]
    , Measure.dataDecls  = [d | DDecl  d <- xs] ++ [d | NTDecl d <- xs]
    , Measure.newtyDecls = [d | NTDecl d <- xs]
    , Measure.aliases    = [a | Alias  a <- xs]
    , Measure.ealiases   = [e | EAlias e <- xs]
    , Measure.embeds     = tceFromList [(c, (fTyconSort tc, a)) | Embed (c, tc, a) <- xs]
    , Measure.qualifiers = [q | Qualif q <- xs]
    , Measure.lvars      = S.fromList [d | LVars d  <- xs]
    , Measure.autois     = S.fromList [s | Insts s <- xs]
    , Measure.pragmas    = [s | Pragma s <- xs]
    , Measure.cmeasures  = [m | CMeas  m <- xs]
    , Measure.imeasures  = [m | IMeas  m <- xs]
    , Measure.omeasures  = []
    , Measure.classes    = [c | Class  c <- xs]
    , Measure.relational = [r | Relational r <- xs]
    , Measure.asmRel     = [r | AssmRel r <- xs]
    , Measure.dvariance  = [v | Varia  v <- xs]
    , Measure.dsize      = [v | DSize  v <- xs]
    , Measure.rinstance  = [i | RInst  i <- xs]
    , Measure.termexprs  = [(y, es) | Asrts (ys, (_, Just es)) <- xs, y <- ys]
    , Measure.lazy       = S.fromList [s | Lazy   s <- xs]
    , Measure.fails      = S.fromList [s | Fail   s <- xs]
    , Measure.rewrites   = S.fromList [s | Rewrite s <- xs]
    , Measure.rewriteWith = M.fromList [s | Rewritewith s <- xs]
    , Measure.bounds     = M.fromList [(bname i, i) | PBound i <- xs]
    , Measure.reflects   = S.fromList [s | Reflect s <- xs]
    , Measure.privateReflects = S.fromList [s | PrivateReflect s <- xs]
    , Measure.opaqueReflects = S.fromList [s | OpaqueReflect s <- xs]
    , Measure.hmeas      = S.fromList [s | HMeas  s <- xs]
    , Measure.inlines    = S.fromList [s | Inline s <- xs]
    , Measure.ignores    = S.fromList [s | Ignore s <- xs]
    , Measure.autosize   = S.fromList [s | ASize  s <- xs]
    , Measure.axeqs      = []
    , Measure.defines    = [ toLMapV d | Define d <- xs]
    , Measure.usedDataCons = mempty
    }
  
  -- | Parse a single top level liquid specification
  specP :: Parser BPspec
  specP
    = fallbackSpecP "assume" ((reserved "reflect" >> fmap AssmReflect assmReflectBindP)
          <|> (reserved "relational" >>  fmap AssmRel relationalP)
          <|>                            fmap Assm   tyBindLHNameP  )
      <|> fallbackSpecP "assert"      (fmap Asrt    tyBindLocalLHNameP)
      <|> fallbackSpecP "autosize"    (fmap ASize   tyConBindLHNameP)
  
      -- TODO: These next two are synonyms, kill one
      <|> fallbackSpecP "axiomatize"  (fmap Reflect locBinderLHNameP)
      <|> fallbackSpecP "reflect"     (fmap Reflect locBinderLHNameP)
      <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )
      <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  )
  
      <|> fallbackSpecP "define"  logDefineP
      <|> fallbackSpecP "measure" hmeasureP
  
      <|> (reserved "infixl"        >> fmap BFix    infixlP  )
      <|> (reserved "infixr"        >> fmap BFix    infixrP  )
      <|> (reserved "infix"         >> fmap BFix    infixP   )
      <|> fallbackSpecP "inline"      (fmap Inline locBinderThisModuleLHNameP)
      <|> fallbackSpecP "ignore"      (fmap Ignore  locBinderThisModuleLHNameP)
  
      <|> fallbackSpecP "bound"       (fmap PBound  boundP)
      <|> (reserved "class"
           >> ((reserved "measure"  >> fmap CMeas  cMeasureP )
           <|> fmap Class  classP                            ))
      <|> (reserved "instance"
           >> ((reserved "measure"  >> fmap IMeas  iMeasureP )
           <|> fmap RInst  instanceP ))
  
      <|> (reserved "data"
          >> ((reserved "variance"  >> fmap Varia  datavarianceP)
          <|> (reserved "size"      >> fmap DSize  dsizeP)
          <|> fmap DDecl  dataDeclP ))
      <|> (reserved "newtype"       >> fmap NTDecl dataDeclP )
      <|> (reserved "relational"    >> fmap Relational relationalP )
      <|> fallbackSpecP "invariant"   (fmap Invt   invariantP)
      <|> (reserved "using"          >> fmap Using invaliasP )
      <|> (reserved "type"          >> fmap Alias  aliasP    )
  
      -- TODO: Next two are basically synonyms
      <|> fallbackSpecP "predicate"   (fmap EAlias ealiasP   )
      <|> fallbackSpecP "expression"  (fmap EAlias ealiasP   )
  
      <|> fallbackSpecP "embed"       (fmap Embed  embedP    )
      <|> fallbackSpecP "qualif"      (fmap Qualif (qualifierP sortP))
      <|> (reserved "lazyvar"       >> fmap LVars  locBinderThisModuleLHNameP)
  
      <|> (reserved "lazy"          >> fmap Lazy   locBinderLHNameP)
      <|> (reserved "rewrite"       >> fmap Rewrite locBinderLHNameP)
      <|> (reserved "rewriteWith"   >> fmap Rewritewith   rewriteWithP )
      <|> (reserved "fail"          >> fmap Fail locBinderThisModuleLHNameP )
      <|> (reserved "ple"           >> fmap Insts locBinderThisModuleLHNameP  )
      <|> (reserved "automatic-instances" >> fmap Insts locBinderThisModuleLHNameP  )
      <|> (reserved "LIQUID"        >> fmap Pragma pragmaP   )
      <|> (reserved "liquid"        >> fmap Pragma pragmaP   )
      <|> {- DEFAULT -}                fmap Asrts  tyBindsP
      <?> "specP"
  
  -- | Try the given parser on the tail after matching the reserved word, and if
  -- it fails fall back to parsing it as a haskell signature for a function with
  -- the same name.
  fallbackSpecP :: String -> Parser BPspec -> Parser BPspec
  fallbackSpecP kw p = do
    (Loc l1 l2 _) <- locReserved kw
    p <|> fmap Asrts (tyBindsRemP (Loc l1 l2 (makeUnresolvedLHName (LHVarName LHThisModuleNameF) (symbol kw))))
  
  -- | Same as tyBindsP, except the single initial symbol has already been matched
  tyBindsRemP
    :: Located LHName
    -> Parser ([Located LHName], (Located BareTypeParsed, Maybe [Located (ExprV LocSymbol)]))
  tyBindsRemP sy = do
    reservedOp "::"
    tb <- termBareTypeP
    return ([sy],tb)
  
  pragmaP :: Parser (Located String)
  pragmaP = locStringLiteral
  
  rewriteWithP :: Parser (Located LHName, [Located LHName])
  rewriteWithP = (,) <$> locBinderLHNameP <*> brackets (sepBy1 locBinderLHNameP comma)
  
  axiomP :: Parser LocSymbol
  axiomP = locBinderP
  
  datavarianceP :: Parser (Located LHName, [Variance])
  datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP)
  
  dsizeP :: Parser ([Located BareTypeParsed], Located Symbol)
  dsizeP = liftM2 (,) (parens $ sepBy (located genBareTypeP) comma) locBinderP
  
  
  varianceP :: Parser Variance
  varianceP = (reserved "bivariant"     >> return Bivariant)
          <|> (reserved "invariant"     >> return Invariant)
          <|> (reserved "covariant"     >> return Covariant)
          <|> (reserved "contravariant" >> return Contravariant)
          <?> "Invalid variance annotation\t Use one of bivariant, invariant, covariant, contravariant"
  
  tyBindsP :: Parser ([Located LHName], (Located BareTypeParsed, Maybe [Located (ExprV LocSymbol)]))
  tyBindsP =
    xyP (sepBy1 locBinderThisModuleLHNameP comma) (reservedOp "::") termBareTypeP
  
  tyBindNoLocP :: Parser (LocSymbol, BareTypeParsed)
  tyBindNoLocP = second val <$> tyBindP
  
  -- | Parses a type signature as it occurs in "assume" and "assert" directives.
  tyBindP :: Parser (LocSymbol, Located BareTypeParsed)
  tyBindP =
    (,) <$> locBinderP <* reservedOp "::" <*> located genBareTypeP
  
  tyBindLogicNameP :: Parser (Located LHName, Located BareTypeParsed)
  tyBindLogicNameP =
    (,) <$> locBinderLogicNameP <* reservedOp "::" <*> located genBareTypeP
  
  tyBindLHNameP :: Parser (Located LHName, Located BareTypeParsed)
  tyBindLHNameP = do
      x <- locBinderLHNameP
      _ <- reservedOp "::"
      t <- located genBareTypeP
      return (x, t)
  
  tyBindLocalLHNameP :: Parser (Located LHName, Located BareTypeParsed)
  tyBindLocalLHNameP = do
      x <- locBinderThisModuleLHNameP
      _ <- reservedOp "::"
      t <- located genBareTypeP
      return (x, t)
  
  -- | Parses a loc symbol.
  assmReflectBindP :: Parser (Located LHName, Located LHName)
  assmReflectBindP =
    (,) <$> locBinderLHNameP <* reservedOp "as" <*> locBinderLHNameP
  
  termBareTypeP :: Parser (Located BareTypeParsed, Maybe [Located (ExprV LocSymbol)])
  termBareTypeP = do
    t <- located genBareTypeP
    termTypeP t <|> return (t, Nothing)
  
  termTypeP :: Located BareTypeParsed -> Parser (Located BareTypeParsed, Maybe [Located (ExprV LocSymbol)])
  termTypeP t
    = do
         reservedOp "/"
         es <- brackets $ sepBy (located exprP) comma
         return (t, Just es)
  
  -- -------------------------------------
  
  invariantP :: Parser (Located BareTypeParsed)
  invariantP = located genBareTypeP
  
  invaliasP :: Parser (Located BareTypeParsed, Located BareTypeParsed)
  invaliasP
    = do t  <- located genBareTypeP
         reserved "as"
         ta <- located genBareTypeP
         return (t, ta)
  
  genBareTypeP :: Parser BareTypeParsed
  genBareTypeP = bareTypeP
  
  embedP :: Parser (Located LHName, FTycon, TCArgs)
  embedP = do
    x <- locUpperIdLHNameP LHTcName
    a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious
    _ <- reserved "as"
    t <- fTyConP
    return (x, t, a)
    --  = xyP locUpperIdP symbolTCArgs (reserved "as") fTyConP
  
  
  aliasP :: Parser (RTAlias Symbol BareTypeParsed)
  aliasP  = rtAliasP id     bareTypeP <?> "aliasP"
  
  ealiasP :: Parser (RTAlias Symbol (ExprV LocSymbol))
  ealiasP = try (rtAliasP symbol predP)
        <|> rtAliasP symbol exprP
        <?> "ealiasP"
  
  -- | Parser for a LH type synonym.
  rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty)
  rtAliasP f bodyP
    = do lname <- locBinderLogicNameP
         args <- many aliasIdP
         reservedOp "="
         body <- bodyP
         let (tArgs, vArgs) = partition (isSmall . headSym) args
         return $ RTA lname (f <$> tArgs) vArgs body
  
  logDefineP :: Parser BPspec
  logDefineP =
      do s <- locBinderLHNameP
         args <- many locSymbolP
         reservedOp "="
         e <- exprP <|> predP
         return (Define (s, (val <$> args, e)))
  
  hmeasureP :: Parser BPspec
  hmeasureP = do
    setLayout
    do b <- try (locBinderLogicNameP <* reservedOp "::")
       ty <- located genBareTypeP
       popLayout >> popLayout
       eqns <- block $ try $ measureDefP LHLogicNameBinder (rawBodyP <|> tyBodyP ty)
       return (Meas $ Measure.mkM b ty eqns MsMeasure mempty)
      <|>
     do b <- locBinderLHNameP
        popLayout >> popLayout >> return (HMeas b)
  
  iMeasureP :: Parser (MeasureV LocSymbol (Located BareTypeParsed) (Located LHName))
  iMeasureP = do
    (x, ty) <- indentedLine tyBindP
    _ <- optional semi
    eqns    <- block $ measureDefP LHLogicName (rawBodyP <|> tyBodyP ty)
    return   $ Measure.mkM (makeUnresolvedLHName LHLogicName <$> x) ty eqns MsMeasure mempty
  
  -- | class measure
  cMeasureP :: Parser (MeasureV LocSymbol (Located BareTypeParsed) ())
  cMeasureP
    = do (x, ty) <- tyBindLogicNameP
         return $ Measure.mkM x ty [] MsClass mempty
  
  oneClassArg :: Parser [Located BareTypeParsed]
  oneClassArg
    = sing <$> located (rit <$> classBTyConP <*> (map val <$> classParams))
    where
      rit t as    = RApp t ((`RVar` trueURef) <$> as) [] trueURef
      classParams =  (reserved "where" >> return [])
                 <|> ((:) <$> ((\ls -> bTyVar ls <$ ls) <$> locLowerIdP) <*> classParams)
      sing x      = [x]
  
  
  superP :: Parser (Located BareTypeParsed)
  superP = located (toRCls <$> bareAtomBindP)
    where toRCls x = x
  
  instanceP :: Parser (RInstance (Located BareTypeParsed))
  instanceP
    = do _    <- supersP
         c    <- classBTyConP
         tvs  <- try oneClassArg <|> manyTill iargsP (try $ reserved "where")
         ms   <- block riMethodSigP
         return $ RI c Nothing tvs ms
    where
      supersP  = try ((parens (superP `sepBy1` comma) <|> fmap pure superP)
                         <* reservedOp "=>")
                 <|> return []
  
      iargsP   =   (mkVar . bTyVar <$> located tyVarIdP)
              <|> parens (located bareTypeP)
  
  
      mkVar v  = dummyLoc $ RVar v (uTop trueReft)
  
  
  riMethodSigP :: Parser (Located LHName, RISig (Located BareTypeParsed))
  riMethodSigP
    = try (do reserved "assume"
              (x, t) <- tyBindLHNameP
              return (x, RIAssumed t) )
   <|> do (x, t) <- tyBindLHNameP
          return (x, RISig t)
   <?> "riMethodSigP"
  
  classP :: Parser (RClass (Located BareTypeParsed))
  classP
    = do sups <- supersP
         c    <- classBTyConP
         tvs  <- manyTill (bTyVar <$> located tyVarIdP) (try $ reserved "where")
         ms   <- block tyBindLHNameP -- <|> sepBy tyBindP semi
         return $ RClass c sups tvs ms
    where
      supersP  = try ((parens (superP `sepBy1` comma) <|> fmap pure superP)
                         <* reservedOp "=>")
                 <|> return []
  
  rawBodyP :: Parser (BodyV LocSymbol)
  rawBodyP
    = braces $ do
        v <- symbolP
        reservedOp "|"
        R v <$> predP
  
  tyBodyP :: Located BareTypeParsed -> Parser (BodyV LocSymbol)
  tyBodyP ty
    = case outTy (val ty) of
        Just bt | isPropBareType bt
                  -> P <$> predP
        _         -> E <$> exprP
      where outTy (RAllT _ t _)    = outTy t
            outTy (RAllP _ t)      = outTy t
            outTy (RFun _ _ _ t _) = Just t
            outTy _                = Nothing
  
  locUpperOrInfixIdP :: Parser (Located Symbol)
  locUpperOrInfixIdP = locUpperIdP' <|> locInfixCondIdP
  
  locBinderP :: Parser (Located Symbol)
  locBinderP =
    located binderP -- TODO
  
  locBinderLogicNameP :: Parser (Located LHName)
  locBinderLogicNameP =
    fmap (makeUnresolvedLHName LHLogicNameBinder) <$> located binderP
  
  locBinderLHNameP :: Parser (Located LHName)
  locBinderLHNameP =
    located $ makeUnresolvedLHName (LHVarName LHAnyModuleNameF) <$> binderP
  
  locBinderThisModuleLHNameP :: Parser (Located LHName)
  locBinderThisModuleLHNameP =
    located $ makeUnresolvedLHName (LHVarName LHThisModuleNameF) <$> binderP
  
  -- | LHS of the thing being defined
  --
  -- TODO, Andres: this is still very broken
  --
  {-
  binderP :: Parser Symbol
  binderP    = pwr    <$> parens (idP bad)
           <|> symbol <$> idP badc
    where
      idP p  = takeWhile1P Nothing (not . p)
      badc c = (c == ':') || (c == ',') || bad c
      bad c  = isSpace c || c `elem` ("(,)[]" :: String)
      pwr s  = symbol $ "(" `mappend` s `mappend` ")"
  -}
  binderP :: Parser Symbol
  binderP =
        parens infixBinderIdP
    <|> binderIdP
    -- Note: It is important that we do *not* use the LH/fixpoint reserved words here,
    -- because, for example, we must be able to use "assert" as an identifier.
  
  measureDefP :: LHNameSpace -> Parser (BodyV LocSymbol) -> Parser (DefV LocSymbol (Located BareTypeParsed) (Located LHName))
  measureDefP ns bodyP
    = do mname   <- fmap (makeUnresolvedLHName ns) <$> locSymbolP
         (c, xs) <- measurePatP
         reservedOp "="
         body    <- bodyP
         let xs'  = symbol . val <$> xs
         return   $ Def mname c Nothing ((, Nothing) <$> xs') body
  
  measurePatP :: Parser (Located LHName, [LocSymbol])
  measurePatP
    =  parens (try conPatP <|> try consPatP <|> nilPatP <|> tupPatP)
   <|> nullaryConPatP
   <?> "measurePatP"
  
  tupPatP :: Parser (Located LHName, [Located Symbol])
  tupPatP  = mkTupPat  <$> located (sepBy1 locLowerIdP comma)
  
  conPatP :: Parser (Located LHName, [Located Symbol])
  conPatP  = (,)       <$> dataConLHNameP <*> many locLowerIdP
  
  consPatP :: Parser (Located LHName, [Located Symbol])
  consPatP = mkConsPat <$> locLowerIdP  <*> located (reservedOp ":") <*> locLowerIdP
  
  nilPatP :: Parser (Located LHName, [t])
  nilPatP  = mkNilPat  <$> located (brackets (pure ()))
  
  nullaryConPatP :: Parser (Located LHName, [t])
  nullaryConPatP = nilPatP <|> ((,[]) <$> dataConLHNameP)
                   <?> "nullaryConPatP"
  
  mkTupPat :: Foldable t => Located (t a) -> (Located LHName, t a)
  mkTupPat lzs =
      let tupledDC = GHC.tupleDataCon GHC.Boxed (length (val lzs))
       in (makeGHCLHName (GHC.getName tupledDC) (symbol tupledDC) <$ lzs, val lzs)
  
  mkNilPat :: Located t -> (Located LHName, [t1])
  mkNilPat lx     = (makeGHCLHName (GHC.getName GHC.nilDataCon) (symbol GHC.nilDataCon) <$ lx, [])
  
  mkConsPat :: t1 -> Located t -> t1 -> (Located LHName, [t1])
  mkConsPat x lc y = (makeGHCLHName (GHC.getName GHC.consDataCon) (symbol GHC.consDataCon) <$ lc, [x, y])
  
  -------------------------------------------------------------------------------
  --------------------------------- Predicates ----------------------------------
  -------------------------------------------------------------------------------
  
  dataConFieldsP :: Parser [(LHName, BareTypeParsed)]
  dataConFieldsP
     = map (first (makeUnresolvedLHName LHLogicNameBinder)) <$>
       (explicitCommaBlock predTypeDDP -- braces (sepBy predTypeDDP comma)
         <|> many dataConFieldP
         <?> "dataConFieldP"
       )
  
  dataConFieldP :: Parser (Symbol, BareTypeParsed)
  dataConFieldP
     =  parens (try predTypeDDP <|> dbTypeP)
    <|> dbTyArgP -- unparenthesised constructor fields must be "atomic"
    <?> "dataConFieldP"
    where
      dbTypeP = (,) <$> dummyBindP <*> bareTypeP
      dbTyArgP = (,) <$> dummyBindP <*> bareTyArgP
  
  predTypeDDP :: Parser (Symbol, BareTypeParsed)
  predTypeDDP = (,) <$> bbindP <*> bareTypeP
  
  bbindP   :: Parser Symbol
  bbindP   = lowerIdP <* reservedOp "::"
  
  tyConBindLHNameP :: Parser (Located LHName)
  tyConBindLHNameP = locUpperIdLHNameP LHTcName
  
  dataConP :: [Symbol] -> Parser DataCtorParsed
  dataConP as = do
    x   <- dataConLHNameP
    xts <- dataConFieldsP
    return $ DataCtor x as [] xts Nothing
  
  adtDataConP :: [Symbol] -> Parser DataCtorParsed
  adtDataConP as = do
    x     <- dataConLHNameP
    reservedOp "::"
    tr    <- toRTypeRep <$> bareTypeP
    return $ DataCtor x (tRepVars as tr) [] (tRepFields tr) (Just $ ty_res tr)
  
  tRepVars :: Symbolic a => [Symbol] -> RTypeRepV v c a r -> [Symbol]
  tRepVars as tr = case fst <$> ty_vars tr of
    [] -> as
    vs -> symbol . ty_var_value <$> vs
  
  tRepFields :: RTypeRepV v c tv r -> [(LHName, RTypeV v c tv r)]
  tRepFields tr = zip (map (makeUnresolvedLHName LHLogicNameBinder) $ ty_binds tr) (ty_args tr)
  
  -- TODO: fix Located
  dataConNameP :: Parser (Located Symbol)
  dataConNameP
    =  located
   (   try upperIdP
   <|> pwr <$> parens (idP bad)
   <?> "dataConNameP"
   )
    where
       idP p  = takeWhile1P Nothing (not . p)
       bad c  = isSpace c || c `elem` ("(,)" :: String)
       pwr s  = symbol s
  
  dataConLHNameP :: Parser (Located LHName)
  dataConLHNameP = fmap (makeUnresolvedLHName (LHDataConName LHAnyModuleNameF)) <$> dataConNameP
  
  dataSizeP :: Parser (Maybe (SizeFunV LocSymbol))
  dataSizeP
    = brackets (Just . SymSizeFun <$> located locLowerIdP)
    <|> return Nothing
  
  relationalP :: Parser (Located LHName, Located LHName, LocBareTypeParsed, LocBareTypeParsed, RelExprV LocSymbol, RelExprV LocSymbol)
  relationalP = do
     x <- locBinderLHNameP
     reserved "~"
     y <- locBinderLHNameP
     reserved "::"
     braces $ do
      tx <- located genBareTypeP
      reserved "~"
      ty <- located genBareTypeP
      reserved "|"
      assm <- try (relrefaP <* reserved "|-") <|> return (ERBasic PTrue)
      ex <- relrefaP
      return (x,y,tx,ty,assm,ex)
  
  dataDeclP :: Parser DataDeclParsed
  dataDeclP = do
    pos <- getSourcePos
    x   <- locUpperOrInfixIdP
    fsize <- dataSizeP
    dataDeclBodyP pos x fsize <|> return (emptyDecl x pos fsize)
  
  emptyDecl :: LocSymbol -> SourcePos -> Maybe (SizeFunV LocSymbol) -> DataDeclParsed
  emptyDecl x pos fsize@(Just _)
    = DataDecl (DnName $ makeUnresolvedLHName LHTcName <$> x) [] [] Nothing pos fsize Nothing DataUser
  emptyDecl x pos _
    = uError (ErrBadData (sourcePosSrcSpan pos) (pprint (val x)) msg)
    where
      msg = "You should specify either a default [size] or one or more fields in the data declaration"
  
  dataDeclBodyP :: SourcePos -> LocSymbol -> Maybe (SizeFunV LocSymbol) -> Parser DataDeclParsed
  dataDeclBodyP pos x fsize = do
    vanilla    <- null <$> many locUpperIdP
    as         <- many noWhere -- TODO: check this again
    ps         <- predVarDefsP
    (pTy, dcs) <- dataCtorsP as
    let dn      = dataDeclName pos x vanilla dcs
    return      $ DataDecl dn as ps (Just dcs) pos fsize pTy DataUser
  
  dataDeclName :: SourcePos -> LocSymbol -> Bool -> [DataCtorParsed] -> DataName
  dataDeclName _ x True  _     = DnName $ makeUnresolvedLHName LHTcName <$> x  -- vanilla data    declaration
  dataDeclName _ _ False (d:_) = DnCon  $ dcName d                             -- family instance declaration
  dataDeclName p x _  _        = uError (ErrBadData (sourcePosSrcSpan p) (pprint (val x)) msg)
    where
      msg                  = "You should specify at least one data constructor for a family instance"
  
  -- | Parse the constructors of a datatype, allowing both classic and GADT-style syntax.
  --
  -- Note that as of 2020-10-14, we changed the syntax of GADT-style datatype declarations
  -- to match Haskell more closely and parse all constructors in a layout-sensitive block,
  -- whereas before we required them to be separated by @|@.
  --
  dataCtorsP :: [Symbol] -> Parser (Maybe BareTypeParsed, [DataCtorParsed])
  dataCtorsP as = do
    (pTy, dcs) <-     (reservedOp "="     >> ((Nothing, ) <$>                 sepBy (dataConP    as) (reservedOp "|")))
                  <|> (reserved   "where" >> ((Nothing, ) <$>                 block (adtDataConP as)                 ))
                  <|>                        ((,)         <$> dataPropTyP <*> block (adtDataConP as)                  )
    return (pTy, Misc.sortOn (val . dcName) dcs)
  
  noWhere :: Parser Symbol
  noWhere =
    try $ do
    s <- tyVarIdP
    guard (s /= "where")
    return s
  
  dataPropTyP :: Parser (Maybe BareTypeParsed)
  dataPropTyP = Just <$> between (reservedOp "::") (reserved "where") bareTypeP
  
  ---------------------------------------------------------------------
  -- Identifiers ------------------------------------------------------
  ---------------------------------------------------------------------
  
  -- Andres, TODO: Fix all the rules for identifiers. This was limited to all lowercase letters before.
  tyVarIdR :: Parser Symbol
  tyVarIdR =
    condIdR (lowerChar <|> char '_') isAlphaNum isNotReserved "unexpected reserved name"
  
  tyVarIdP :: Parser Symbol
  tyVarIdP =
    lexeme tyVarIdR
  
  aliasIdR :: Parser Symbol
  aliasIdR =
    condIdR (letterChar <|> char '_') isAlphaNum (const True) "unexpected"
  
  aliasIdP :: Parser Symbol
  aliasIdP =
    lexeme aliasIdR
  
  -- | Andres, TODO: This must be liberal with respect to reserved words (LH reserved words are
  -- not Haskell reserved words, and we want to redefine all sorts of internal stuff).
  --
  -- Also, this currently accepts qualified names by allowing '.' ...
  -- Moreover, it seems that it is currently allowed to use qualified symbolic names in
  -- unparenthesised form. Oh, the parser is also used for reflect, where apparently
  -- symbolic names appear in unqualified and unparenthesised form.
  -- Furthermore, : is explicitly excluded because a : can directly, without whitespace,
  -- follow a binder ...
  --
  binderIdR :: Parser Symbol
  binderIdR =
    condIdR (letterChar <|> char '_' <|> satisfy isHaskellOpStartChar) (\ c -> isAlphaNum c || isHaskellOpStartChar c || c `elem` ("_'" :: String)) (const True) "unexpected"
  
  binderIdP :: Parser Symbol
  binderIdP =
    lexeme binderIdR
  
  infixBinderIdR :: Parser Symbol
  infixBinderIdR =
    condIdR (letterChar <|> char '_' <|> satisfy isHaskellOpChar) (\ c -> isAlphaNum c || isHaskellOpChar c || c `elem` ("_'" :: String)) (const True) "unexpected"
  
  infixBinderIdP :: Parser Symbol
  infixBinderIdP =
    lexeme infixBinderIdR
  
  upperIdR' :: Parser Symbol
  upperIdR' =
    condIdR upperChar (\ c -> isAlphaNum c || c == '\'') (const True) "unexpected"
  
  locUpperIdP' :: Parser (Located Symbol)
  locUpperIdP' =
    locLexeme upperIdR'
  
  -- Andres, TODO: This used to force a colon at the end. Also, it used to not
  -- allow colons in the middle. Finally, it should probably exclude all reserved
  -- operators. I'm just excluding :: because I'm pretty sure that would be
  -- undesired.
  --
  infixCondIdR :: Parser Symbol
  infixCondIdR =
    condIdR (char ':') isHaskellOpChar (/= "::") "unexpected double colon"
  
  -- Andres, TODO: This used to be completely ad-hoc. It's still not good though.
  infixIdR :: Parser Symbol
  infixIdR =
    condIdR (satisfy isHaskellOpChar) isHaskellOpChar (/= "::") "unexpected double colon"
  
  infixIdP :: Parser Symbol
  infixIdP =
    lexeme infixIdR
  
  {-
  infixVarIdR :: Parser Symbol
  infixVarIdR =
    condIdR (satisfy isHaskellOpStartChar) isHaskellOpChar (const True)
  
  infixVarIdP :: Parser Symbol
  infixVarIdP =
    lexeme infixVarIdR
  -}
  
  isHaskellOpChar :: Char -> Bool
  isHaskellOpChar c
    = c `elem` (":!#$%&*+./<=>?@\\^|~-" :: String)
  
  isHaskellOpStartChar :: Char -> Bool
  isHaskellOpStartChar c
    = c `elem` ("!#$%&*+./<=>?@\\^|~-" :: String)
  
  locInfixCondIdP :: Parser (Located Symbol)
  locInfixCondIdP =
    locLexeme infixCondIdR
  