    -- See Note [-Wincomplete-uni-patterns and irrefutable patterns]
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.TypePat
      ( aInf, aNat, aNat'

      , anAdd, (|-|), aMul, (|^|), (|/|), (|%|)
      , aMin, aMax
      , aWidth
      , aCeilDiv, aCeilMod
      , aLenFromThenTo

      , aLiteral
      , aLiteralLessThan
      , aLogic

      , aTVar
      , aFreeTVar
      , anAbstractType
      , aBit
      , aSeq
      , aWord
      , aChar
      , aTuple
      , aRec
      , (|->|)

      , aFin, (|=|), (|/=|), (|>=|)
      , aAnd
      , aTrue

      , anError

      , module Cryptol.Utils.Patterns
      ) where

    import Control.Applicative((<|>))
    import Control.Monad
    import Cryptol.Utils.Ident (Ident)
    import Cryptol.Utils.Patterns
    import Cryptol.Utils.RecordMap
    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.Solver.InfNat

    tcon :: TCon -> ([Type] -> a) -> Pat Type a
    tcon :: forall a. TCon -> ([Type] -> a) -> Pat Type a
    tcon TCon
    f [Type] -> a
    p = \Type
    ty -> case Type -> Type
    tNoUser Type
    ty of
                        TCon TCon
    c [Type]
    ts | TCon
    f TCon -> TCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TCon
    c -> a -> Match a
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> a
    p [Type]
    ts)
                        Type
    _                  -> Match a
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    ar0 :: [a] -> ()
    ar0 :: forall a. [a] -> ()
    ar0 ~[] = ()

    ar1 :: [a] -> a
    ar1 :: forall a. [a] -> a
    ar1 ~[a
    a] = a
    a

    ar2 :: [a] -> (a,a)
    ar2 :: forall a. [a] -> (a, a)
    ar2 ~[a
    a,a
    b] = (a
    a,a
    b)

    ar3 :: [a] -> (a,a,a)
    ar3 :: forall a. [a] -> (a, a, a)
    ar3 ~[a
    a,a
    b,a
    c] = (a
    a,a
    b,a
    c)

    tf :: TFun -> ([Type] -> a) -> Pat Type a
    tf :: forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    f [Type] -> a
    ar = TCon -> ([Type] -> a) -> Pat Type a
    forall a. TCon -> ([Type] -> a) -> Pat Type a
    tcon (TFun -> TCon
    TF TFun
    f) [Type] -> a
    ar

    tc :: TC -> ([Type] -> a) -> Pat Type a
    tc :: forall a. TC -> ([Type] -> a) -> Pat Type a
    tc TC
    f [Type] -> a
    ar = TCon -> ([Type] -> a) -> Pat Type a
    forall a. TCon -> ([Type] -> a) -> Pat Type a
    tcon (TC -> TCon
    TC TC
    f) [Type] -> a
    ar

    tp :: PC -> ([Type] -> a) -> Pat Prop a
    tp :: forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    f [Type] -> a
    ar = TCon -> ([Type] -> a) -> Pat Type a
    forall a. TCon -> ([Type] -> a) -> Pat Type a
    tcon (PC -> TCon
    PC PC
    f) [Type] -> a
    ar

    --------------------------------------------------------------------------------

    aInf :: Pat Type ()
    aInf :: Pat Type ()
    aInf = TC -> ([Type] -> ()) -> Pat Type ()
    forall a. TC -> ([Type] -> a) -> Pat Type a
    tc TC
    TCInf [Type] -> ()
    forall a. [a] -> ()
    ar0

    aNat :: Pat Type Integer
    aNat :: Pat Type Integer
    aNat = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                   TCon (TC (TCNum Integer
    n)) [Type]
    _ -> Integer -> Match Integer
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    n
                   Type
    _                     -> Match Integer
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    aNat' :: Pat Type Nat'
    aNat' :: Pat Type Nat'
    aNat' = \Type
    a -> (Nat'
    Inf Nat' -> Match () -> Match Nat'
    forall a b. a -> Match b -> Match a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$  Pat Type ()
    aInf Type
    a)
              Match Nat' -> Match Nat' -> Match Nat'
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Integer -> Nat'
    Nat (Integer -> Nat') -> Match Integer -> Match Nat'
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pat Type Integer
    aNat Type
    a)

    anAdd :: Pat Type (Type,Type)
    anAdd :: Pat Type (Type, Type)
    anAdd = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCAdd [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|-|) :: Pat Type (Type,Type)
    |-| :: Pat Type (Type, Type)
    (|-|) = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCSub [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aMul :: Pat Type (Type,Type)
    aMul :: Pat Type (Type, Type)
    aMul = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCMul [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|^|) :: Pat Type (Type,Type)
    |^| :: Pat Type (Type, Type)
    (|^|) = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCExp [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|/|) :: Pat Type (Type,Type)
    |/| :: Pat Type (Type, Type)
    (|/|) = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCDiv [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|%|) :: Pat Type (Type,Type)
    |%| :: Pat Type (Type, Type)
    (|%|) = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCMod [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aMin :: Pat Type (Type,Type)
    aMin :: Pat Type (Type, Type)
    aMin = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCMin [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aMax :: Pat Type (Type,Type)
    aMax :: Pat Type (Type, Type)
    aMax = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCMax [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aWidth :: Pat Type Type
    aWidth :: Pat Type Type
    aWidth = TFun -> ([Type] -> Type) -> Pat Type Type
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCWidth [Type] -> Type
    forall a. [a] -> a
    ar1

    aCeilDiv :: Pat Type (Type,Type)
    aCeilDiv :: Pat Type (Type, Type)
    aCeilDiv = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCCeilDiv [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aCeilMod :: Pat Type (Type,Type)
    aCeilMod :: Pat Type (Type, Type)
    aCeilMod = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCCeilMod [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aLenFromThenTo :: Pat Type (Type,Type,Type)
    aLenFromThenTo :: Pat Type (Type, Type, Type)
    aLenFromThenTo = TFun
    -> ([Type] -> (Type, Type, Type)) -> Pat Type (Type, Type, Type)
    forall a. TFun -> ([Type] -> a) -> Pat Type a
    tf TFun
    TCLenFromThenTo [Type] -> (Type, Type, Type)
    forall a. [a] -> (a, a, a)
    ar3

    --------------------------------------------------------------------------------
    aTVar :: Pat Type TVar
    aTVar :: Pat Type TVar
    aTVar = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                    TVar TVar
    x -> TVar -> Match TVar
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TVar
    x
                    Type
    _      -> Match TVar
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    anAbstractType :: Pat Type UserTC
    anAbstractType :: Pat Type UserTC
    anAbstractType = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                             TCon (TC (TCAbstract UserTC
    ut)) [] -> UserTC -> Match UserTC
    forall a. a -> Match a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure UserTC
    ut
                             Type
    _                            -> Match UserTC
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    aFreeTVar :: Pat Type TVar
    aFreeTVar :: Pat Type TVar
    aFreeTVar Type
    t =
      do TVar
    v <- Pat Type TVar
    aTVar Type
    t
         Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar -> Bool
    isFreeTV TVar
    v)
         TVar -> Match TVar
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TVar
    v

    aBit :: Pat Type ()
    aBit :: Pat Type ()
    aBit = TC -> ([Type] -> ()) -> Pat Type ()
    forall a. TC -> ([Type] -> a) -> Pat Type a
    tc TC
    TCBit [Type] -> ()
    forall a. [a] -> ()
    ar0

    aSeq :: Pat Type (Type,Type)
    aSeq :: Pat Type (Type, Type)
    aSeq = TC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TC -> ([Type] -> a) -> Pat Type a
    tc TC
    TCSeq [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aWord :: Pat Type Type
    aWord :: Pat Type Type
    aWord = \Type
    a -> do (Type
    l,Type
    t) <- Pat Type (Type, Type)
    aSeq Type
    a
                     Pat Type ()
    aBit Type
    t
                     Pat Type Type
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    l

    aChar :: Pat Type ()
    aChar :: Pat Type ()
    aChar = \Type
    a -> do (Type
    l,Type
    t) <- Pat Type (Type, Type)
    aSeq Type
    a
                     Integer
    n     <- Pat Type Integer
    aNat Type
    l
                     Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    8)
                     Pat Type ()
    aBit Type
    t

    aTuple :: Pat Type [Type]
    aTuple :: Pat Type [Type]
    aTuple = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                     TCon (TC (TCTuple Int
    _)) [Type]
    ts -> [Type] -> Match [Type]
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Type]
    ts
                     Type
    _                        -> Match [Type]
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    aRec :: Pat Type (RecordMap Ident Type)
    aRec :: Pat Type (RecordMap Ident Type)
    aRec = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                   TRec RecordMap Ident Type
    fs -> RecordMap Ident Type -> Match (RecordMap Ident Type)
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RecordMap Ident Type
    fs
                   Type
    _       -> Match (RecordMap Ident Type)
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    (|->|) :: Pat Type (Type,Type)
    |->| :: Pat Type (Type, Type)
    (|->|) = TC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. TC -> ([Type] -> a) -> Pat Type a
    tc TC
    TCFun [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2
    --------------------------------------------------------------------------------

    aFin :: Pat Prop Type
    aFin :: Pat Type Type
    aFin = PC -> ([Type] -> Type) -> Pat Type Type
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PFin [Type] -> Type
    forall a. [a] -> a
    ar1

    (|=|) :: Pat Prop (Type,Type)
    |=| :: Pat Type (Type, Type)
    (|=|) = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PEqual [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|/=|) :: Pat Prop (Type,Type)
    |/=| :: Pat Type (Type, Type)
    (|/=|) = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PNeq [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    (|>=|) :: Pat Prop (Type,Type)
    |>=| :: Pat Type (Type, Type)
    (|>=|) = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PGeq [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aAnd :: Pat Prop (Prop,Prop)
    aAnd :: Pat Type (Type, Type)
    aAnd = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PAnd [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aTrue :: Pat Prop ()
    aTrue :: Pat Type ()
    aTrue = PC -> ([Type] -> ()) -> Pat Type ()
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PTrue [Type] -> ()
    forall a. [a] -> ()
    ar0

    aLiteral :: Pat Prop (Type,Type)
    aLiteral :: Pat Type (Type, Type)
    aLiteral = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PLiteral [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aLiteralLessThan :: Pat Prop (Type,Type)
    aLiteralLessThan :: Pat Type (Type, Type)
    aLiteralLessThan = PC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PLiteralLessThan [Type] -> (Type, Type)
    forall a. [a] -> (a, a)
    ar2

    aLogic :: Pat Prop Type
    aLogic :: Pat Type Type
    aLogic = PC -> ([Type] -> Type) -> Pat Type Type
    forall a. PC -> ([Type] -> a) -> Pat Type a
    tp PC
    PLogic [Type] -> Type
    forall a. [a] -> a
    ar1

    --------------------------------------------------------------------------------
    anError :: Kind -> Pat Type ()
    anError :: Kind -> Pat Type ()
    anError Kind
    k = \Type
    a -> case Type -> Type
    tNoUser Type
    a of
                        TCon (TError (Kind
    _ :-> Kind
    k1) ) [Type]
    _ | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k1 -> () -> Match ()
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                        Type
    _                                     -> Match ()
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    {-
    Note [-Wincomplete-uni-patterns and irrefutable patterns]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Various parts of Cryptol use irrefutable patterns in functions that assume that
    their arguments have particular shapes. For example, the `ar1 ~[a] = a`
    function in this module uses an irrefutable pattern because it assumes the
    invariant that the argument list will have exactly one element. This lets ar1
    be slightly lazier when evaluated.

    Unfortunately, this use of irrefutable patterns is at odds with the
    -Wincomplete-uni-patterns warning. At present, -Wincomplete-uni-patterns will
    produce a warning for any irrefutable pattern that does not cover all possible
    data constructors. While we could rewrite functions like `ar1` to explicitly
    provide a fall-through case, that would change its strictness properties. As
    a result, we simply disable -Wincomplete-uni-patterns warnings in each part
    of Cryptol that uses irrefutable patterns.

    Arguably, -Wincomplete-uni-patterns shouldn't be producing warnings for
    irrefutable patterns at all. GHC issue #14800
    (https://gitlab.haskell.org/ghc/ghc/-/issues/14800) proposes this idea.
    If that issue is fixed in the future, we may want to reconsider whether we want
    to disable -Wincomplete-uni-patterns.
    -}