    -- |
    -- Module      :  Cryptol.TypeCheck.Solver.Selector
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    {-# LANGUAGE PatternGuards #-}
    module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where

    import Cryptol.Parser.Position(Range)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.InferTypes
    import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
                                  , newType, applySubst, solveHasGoal
                                  , newLocalName
                                  )
    import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
    import Cryptol.Utils.Ident (Ident, packIdent,Namespace(..))
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.RecordMap

    import Control.Monad(forM,guard)

    recordType :: [Ident] -> InferM Type
    recordType :: [Ident] -> InferM Prop
    recordType [Ident]
    labels =
      do [(Ident, Prop)]
    fields <- [Ident]
    -> (Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Ident]
    labels ((Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)])
    -> (Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)]
    forall a b. (a -> b) -> a -> b
    $ \Ident
    l ->
            do Prop
    t <- TypeSource -> Kind -> InferM Prop
    newType (Ident -> TypeSource
    TypeOfRecordField Ident
    l) Kind
    KType
               (Ident, Prop) -> InferM (Ident, Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ident
    l,Prop
    t)
         Prop -> InferM Prop
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordMap Ident Prop -> Prop
    TRec ([(Ident, Prop)] -> RecordMap Ident Prop
    forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
    recordFromFields [(Ident, Prop)]
    fields))

    tupleType :: Int -> InferM Type
    tupleType :: Int -> InferM Prop
    tupleType Int
    n =
      do [Prop]
    fields <- (Int -> InferM Prop) -> [Int] -> InferM [Prop]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\Int
    x -> TypeSource -> Kind -> InferM Prop
    newType (Int -> TypeSource
    TypeOfTupleField Int
    x) Kind
    KType)
                        [ Int
    0 .. (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) ]
         Prop -> InferM Prop
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Prop] -> Prop
    tTuple [Prop]
    fields)

    listType :: Int -> InferM Type
    listType :: Int -> InferM Prop
    listType Int
    n =
      do Prop
    elems <- TypeSource -> Kind -> InferM Prop
    newType TypeSource
    TypeOfSeqElement Kind
    KType
         Prop -> InferM Prop
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Prop -> Prop
    tSeq (Int -> Prop
    forall a. Integral a => a -> Prop
    tNum Int
    n) Prop
    elems)

    improveSelector :: Maybe Range -> Selector -> Type -> InferM Bool
    improveSelector :: Maybe Range -> Selector -> Prop -> InferM Bool
    improveSelector Maybe Range
    rng Selector
    sel Prop
    outerT =
      case Selector
    sel of
        RecordSel Ident
    _ Maybe [Ident]
    mb -> ([Ident] -> InferM Prop) -> Maybe [Ident] -> InferM Bool
    forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
    cvt [Ident] -> InferM Prop
    recordType Maybe [Ident]
    mb
        TupleSel  Int
    _ Maybe Int
    mb -> (Int -> InferM Prop) -> Maybe Int -> InferM Bool
    forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
    cvt Int -> InferM Prop
    tupleType  Maybe Int
    mb
        ListSel   Int
    _ Maybe Int
    mb -> (Int -> InferM Prop) -> Maybe Int -> InferM Bool
    forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
    cvt Int -> InferM Prop
    listType   Maybe Int
    mb
      where
      cvt :: (t -> InferM Prop) -> Maybe t -> InferM Bool
    cvt t -> InferM Prop
    _ Maybe t
    Nothing   = Bool -> InferM Bool
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      cvt t -> InferM Prop
    f (Just t
    a)  = do Prop
    ty <- t -> InferM Prop
    f t
    a
                           [Prop]
    ps <- TypeWithSource -> Prop -> InferM [Prop]
    unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
    WithSource Prop
    outerT (Selector -> TypeSource
    selSrc Selector
    sel) Maybe Range
    rng) Prop
    ty
                           ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtExactType [Prop]
    ps
                           Prop
    newT <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    outerT
                           Bool -> InferM Bool
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop
    newT Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Prop
    outerT)

    {- | Compute the type of a field based on the selector.
    The given type should be "zonked" (i.e., substitution was applied to it),
    and (outermost) type synonyms have been expanded.
    -}
    solveSelector :: Selector -> Type -> InferM (Maybe Type)
    solveSelector :: Selector -> Prop -> InferM (Maybe Prop)
    solveSelector Selector
    sel Prop
    outerT =
      case (Selector
    sel, Prop
    outerT) of

        (RecordSel Ident
    l Maybe [Ident]
    _, Prop
    ty) ->
          case Prop
    ty of
            TRec RecordMap Ident Prop
    fs -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ident -> RecordMap Ident Prop -> Maybe Prop
    forall a b. Ord a => a -> RecordMap a b -> Maybe b
    lookupField Ident
    l RecordMap Ident Prop
    fs)
            TNewtype Newtype
    nt [Prop]
    ts ->
              case Ident -> RecordMap Ident Prop -> Maybe Prop
    forall a b. Ord a => a -> RecordMap a b -> Maybe b
    lookupField Ident
    l (Newtype -> RecordMap Ident Prop
    ntFields Newtype
    nt) of
                Maybe Prop
    Nothing -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Prop
    forall a. Maybe a
    Nothing
                Just Prop
    t ->
                  do let su :: Subst
    su = [(TParam, Prop)] -> Subst
    listParamSubst ([TParam] -> [Prop] -> [(TParam, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Newtype -> [TParam]
    ntParams Newtype
    nt) [Prop]
    ts)
                     ConstraintSource -> [Prop] -> InferM ()
    newGoals (Name -> ConstraintSource
    CtPartialTypeFun (Newtype -> Name
    ntName Newtype
    nt))
                       ([Prop] -> InferM ()) -> [Prop] -> InferM ()
    forall a b. (a -> b) -> a -> b
    $ Subst -> [Prop] -> [Prop]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su ([Prop] -> [Prop]) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> a -> b
    $ Newtype -> [Prop]
    ntConstraints Newtype
    nt
                     Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Prop -> InferM (Maybe Prop))
    -> Maybe Prop -> InferM (Maybe Prop)
    forall a b. (a -> b) -> a -> b
    $ Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just (Prop -> Maybe Prop) -> Prop -> Maybe Prop
    forall a b. (a -> b) -> a -> b
    $ Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Prop
    t

            TCon (TC TC
    TCSeq) [Prop
    len,Prop
    el] -> Prop -> Prop -> InferM (Maybe Prop)
    liftSeq Prop
    len Prop
    el
            TCon (TC TC
    TCFun) [Prop
    t1,Prop
    t2]  -> Prop -> Prop -> InferM (Maybe Prop)
    liftFun Prop
    t1 Prop
    t2
            Prop
    _ -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Prop
    forall a. Maybe a
    Nothing

        (TupleSel Int
    n Maybe Int
    _, Prop
    ty) ->
          case Prop
    ty of

            TCon (TC (TCTuple Int
    m)) [Prop]
    ts ->
              Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Prop -> InferM (Maybe Prop))
    -> Maybe Prop -> InferM (Maybe Prop)
    forall a b. (a -> b) -> a -> b
    $ do Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Int
    0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    n Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    m)
                          Prop -> Maybe Prop
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Maybe Prop) -> Prop -> Maybe Prop
    forall a b. (a -> b) -> a -> b
    $ [Prop]
    ts [Prop] -> Int -> Prop
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n

            TCon (TC TC
    TCSeq) [Prop
    len,Prop
    el] -> Prop -> Prop -> InferM (Maybe Prop)
    liftSeq Prop
    len Prop
    el
            TCon (TC TC
    TCFun) [Prop
    t1,Prop
    t2]  -> Prop -> Prop -> InferM (Maybe Prop)
    liftFun Prop
    t1 Prop
    t2

            Prop
    _ -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Prop
    forall a. Maybe a
    Nothing

        (ListSel Int
    n Maybe Int
    _, TCon (TC TC
    TCSeq) [Prop
    l,Prop
    t])
          | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    2 -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t)
          | Bool
    otherwise ->
           do ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtSelector [ Prop
    l Prop -> Prop -> Prop
    >== Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) ]
              Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t)

        (Selector, Prop)
    _ -> Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Prop
    forall a. Maybe a
    Nothing

      where
      liftSeq :: Prop -> Prop -> InferM (Maybe Prop)
    liftSeq Prop
    len Prop
    el =
        do Maybe Prop
    mb <- Selector -> Prop -> InferM (Maybe Prop)
    solveSelector Selector
    sel (Prop -> Prop
    tNoUser Prop
    el)
           Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Prop -> InferM (Maybe Prop))
    -> Maybe Prop -> InferM (Maybe Prop)
    forall a b. (a -> b) -> a -> b
    $ do Prop
    el' <- Maybe Prop
    mb
                       Prop -> Maybe Prop
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCSeq) [Prop
    len,Prop
    el'])

      liftFun :: Prop -> Prop -> InferM (Maybe Prop)
    liftFun Prop
    t1 Prop
    t2 =
        do Maybe Prop
    mb <- Selector -> Prop -> InferM (Maybe Prop)
    solveSelector Selector
    sel (Prop -> Prop
    tNoUser Prop
    t2)
           Maybe Prop -> InferM (Maybe Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Prop -> InferM (Maybe Prop))
    -> Maybe Prop -> InferM (Maybe Prop)
    forall a b. (a -> b) -> a -> b
    $ do Prop
    t2' <- Maybe Prop
    mb
                       Prop -> Maybe Prop
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC TC
    TCFun) [Prop
    t1,Prop
    t2'])

    -- | Solve has-constraints.
    tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved
    tryHasGoal :: HasGoal -> InferM (Bool, Bool)
    tryHasGoal HasGoal
    has
      | TCon (PC (PHas Selector
    sel)) [ Prop
    th, Prop
    ft ] <- Goal -> Prop
    goal (HasGoal -> Goal
    hasGoal HasGoal
    has) =
        do let rng :: Maybe Range
    rng = Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Goal -> Range
    goalRange (HasGoal -> Goal
    hasGoal HasGoal
    has))
           Bool
    imped     <- Maybe Range -> Selector -> Prop -> InferM Bool
    improveSelector Maybe Range
    rng Selector
    sel Prop
    th
           Prop
    outerT    <- Prop -> Prop
    tNoUser (Prop -> Prop) -> InferM Prop -> InferM Prop
    forall a b. (a -> b) -> InferM a -> InferM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    th
           Maybe Prop
    mbInnerT  <- Selector -> Prop -> InferM (Maybe Prop)
    solveSelector Selector
    sel Prop
    outerT
           case Maybe Prop
    mbInnerT of
             Maybe Prop
    Nothing -> (Bool, Bool) -> InferM (Bool, Bool)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    imped, Bool
    False)
             Just Prop
    innerT ->
               do ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                                      TypeWithSource -> Prop -> InferM [Prop]
    unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
    WithSource Prop
    innerT (Selector -> TypeSource
    selSrc Selector
    sel) Maybe Range
    rng) Prop
    ft
                  Prop
    oT <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    outerT
                  Prop
    iT <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    innerT
                  HasGoalSln
    sln <- Selector -> Prop -> Prop -> InferM HasGoalSln
    mkSelSln Selector
    sel Prop
    oT Prop
    iT
                  Int -> HasGoalSln -> InferM ()
    solveHasGoal (HasGoal -> Int
    hasName HasGoal
    has) HasGoalSln
    sln
                  (Bool, Bool) -> InferM (Bool, Bool)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, Bool
    True)

      | Bool
    otherwise = String -> [String] -> InferM (Bool, Bool)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "hasGoalSolved"
                      [ String
    "Unexpected selector proposition:"
                      , Goal -> String
    forall a. Show a => a -> String
    show (HasGoal -> Goal
    hasGoal HasGoal
    has)
                      ]

    {- | Generator an appropriate selector, once the "Has" constraint
    has been discharged.  The resulting selectors should always work
    on their corresponding types (i.e., tuple selectros only select from tuples).
    This function generates the code for lifting tuple/record selectors to sequences
    and functions.

    Assumes types are zonked. -}
    mkSelSln :: Selector -> Type -> Type -> InferM HasGoalSln
    mkSelSln :: Selector -> Prop -> Prop -> InferM HasGoalSln
    mkSelSln Selector
    s Prop
    outerT Prop
    innerT =
      case Prop -> Prop
    tNoUser Prop
    outerT of
        TCon (TC TC
    TCSeq) [Prop
    len,Prop
    el]
          | TupleSel {} <- Selector
    s  -> Prop -> Prop -> InferM HasGoalSln
    liftSeq Prop
    len Prop
    el
          | RecordSel {} <- Selector
    s -> Prop -> Prop -> InferM HasGoalSln
    liftSeq Prop
    len Prop
    el

        TCon (TC TC
    TCFun) [Prop
    t1,Prop
    t2]
          | TupleSel {} <- Selector
    s -> Prop -> Prop -> InferM HasGoalSln
    liftFun Prop
    t1 Prop
    t2
          | RecordSel {} <- Selector
    s -> Prop -> Prop -> InferM HasGoalSln
    liftFun Prop
    t1 Prop
    t2

        Prop
    _ -> HasGoalSln -> InferM HasGoalSln
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HasGoalSln { hasDoSelect :: Expr -> Expr
    hasDoSelect = \Expr
    e -> Expr -> Selector -> Expr
    ESel Expr
    e Selector
    s
                               , hasDoSet :: Expr -> Expr -> Expr
    hasDoSet    = \Expr
    e Expr
    v -> Prop -> Expr -> Selector -> Expr -> Expr
    ESet Prop
    outerT Expr
    e Selector
    s Expr
    v }

      where
      -- Has s a t => Has s ([n]a) ([n]t)
      -- xs.s             ~~> [ x.s           | x <- xs ]
      -- { xs | s = ys }  ~~> [ { x | s = y } | x <- xs | y <- ys ]
      liftSeq :: Prop -> Prop -> InferM HasGoalSln
    liftSeq Prop
    len Prop
    el =
        do Name
    x1 <- Namespace -> Ident -> InferM Name
    newLocalName Namespace
    NSValue (String -> Ident
    packIdent String
    "x")
           Name
    x2 <- Namespace -> Ident -> InferM Name
    newLocalName Namespace
    NSValue (String -> Ident
    packIdent String
    "x")
           Name
    y2 <- Namespace -> Ident -> InferM Name
    newLocalName Namespace
    NSValue (String -> Ident
    packIdent String
    "y")
           case Prop -> Prop
    tNoUser Prop
    innerT of
             TCon TCon
    _ [Prop
    _,Prop
    eli] ->
               do HasGoalSln
    d <- Selector -> Prop -> Prop -> InferM HasGoalSln
    mkSelSln Selector
    s Prop
    el Prop
    eli
                  HasGoalSln -> InferM HasGoalSln
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure HasGoalSln
                    { hasDoSelect :: Expr -> Expr
    hasDoSelect = \Expr
    e ->
                        Prop -> Prop -> Expr -> [[Match]] -> Expr
    EComp Prop
    len Prop
    eli (HasGoalSln -> Expr -> Expr
    hasDoSelect HasGoalSln
    d (Name -> Expr
    EVar Name
    x1))
                                      [[ Name -> Prop -> Prop -> Expr -> Match
    From Name
    x1 Prop
    len Prop
    el Expr
    e ]]
                    , hasDoSet :: Expr -> Expr -> Expr
    hasDoSet = \Expr
    e Expr
    v ->
                        Prop -> Prop -> Expr -> [[Match]] -> Expr
    EComp Prop
    len Prop
    el  (HasGoalSln -> Expr -> Expr -> Expr
    hasDoSet HasGoalSln
    d (Name -> Expr
    EVar Name
    x2) (Name -> Expr
    EVar Name
    y2))
                                      [ [ Name -> Prop -> Prop -> Expr -> Match
    From Name
    x2 Prop
    len Prop
    el  Expr
    e ]
                                      , [ Name -> Prop -> Prop -> Expr -> Match
    From Name
    y2 Prop
    len Prop
    eli Expr
    v ]
                                      ]
                    }

             Prop
    _ -> String -> [String] -> InferM HasGoalSln
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "mkSelSln" [ String
    "Unexpected inner seq type.", Prop -> String
    forall a. Show a => a -> String
    show Prop
    innerT ]

      -- Has s b t => Has s (a -> b) (a -> t)
      -- f.s            ~~> \x -> (f x).s
      -- { f | s = g }  ~~> \x -> { f x | s = g x }
      liftFun :: Prop -> Prop -> InferM HasGoalSln
    liftFun Prop
    t1 Prop
    t2 =
        do Name
    x1 <- Namespace -> Ident -> InferM Name
    newLocalName Namespace
    NSValue (String -> Ident
    packIdent String
    "x")
           Name
    x2 <- Namespace -> Ident -> InferM Name
    newLocalName Namespace
    NSValue (String -> Ident
    packIdent String
    "x")
           case Prop -> Prop
    tNoUser Prop
    innerT of
             TCon TCon
    _ [Prop
    _,Prop
    inT] ->
               do HasGoalSln
    d <- Selector -> Prop -> Prop -> InferM HasGoalSln
    mkSelSln Selector
    s Prop
    t2 Prop
    inT
                  HasGoalSln -> InferM HasGoalSln
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure HasGoalSln
                    { hasDoSelect :: Expr -> Expr
    hasDoSelect = \Expr
    e ->
                        Name -> Prop -> Expr -> Expr
    EAbs Name
    x1 Prop
    t1 (HasGoalSln -> Expr -> Expr
    hasDoSelect HasGoalSln
    d (Expr -> Expr -> Expr
    EApp Expr
    e (Name -> Expr
    EVar Name
    x1)))
                    , hasDoSet :: Expr -> Expr -> Expr
    hasDoSet = \Expr
    e Expr
    v ->
                        Name -> Prop -> Expr -> Expr
    EAbs Name
    x2 Prop
    t1 (HasGoalSln -> Expr -> Expr -> Expr
    hasDoSet HasGoalSln
    d (Expr -> Expr -> Expr
    EApp Expr
    e (Name -> Expr
    EVar Name
    x2))
                                               (Expr -> Expr -> Expr
    EApp Expr
    v (Name -> Expr
    EVar Name
    x2))) }
             Prop
    _ -> String -> [String] -> InferM HasGoalSln
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "mkSelSln" [ String
    "Unexpected inner fun type", Prop -> String
    forall a. Show a => a -> String
    show Prop
    innerT ]