-- |
-- Module      :  Cryptol.TypeCheck.Unify
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards, ViewPatterns #-}
{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-}
{-# LANGUAGE BlockArguments, OverloadedStrings #-}
module Cryptol.TypeCheck.Unify where

import Control.DeepSeq(NFData)
import GHC.Generics(Generic)

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.Utils.RecordMap
import Cryptol.Utils.Ident(Ident)
import Cryptol.ModuleSystem.Name(nameIdent)

import Cryptol.TypeCheck.PP
import Control.Monad.Writer (Writer, writer, runWriter)
import qualified Data.Set as Set

import Prelude ()
import Prelude.Compat

-- | The most general unifier is a substitution and a set of constraints
-- on bound variables.
type MGU = (Subst,[Prop])

type Result a = Writer [(Path,UnificationError)] a

runResult :: Result a -> (a, [(Path,UnificationError)])
runResult :: forall a. Result a -> (a, [(Path, UnificationError)])
runResult = Writer [(Path, UnificationError)] a
-> (a, [(Path, UnificationError)])
forall w a. Writer w a -> (a, w)
runWriter

data UnificationError
  = UniTypeMismatch Type Type
  | UniKindMismatch Kind Kind
  | UniTypeLenMismatch Int Int
  | UniRecursive TVar Type
  | UniNonPolyDepends TVar [TParam]
  | UniNonPoly TVar Type

uniError :: Path -> UnificationError -> Result MGU
uniError :: Path -> UnificationError -> Result MGU
uniError Path
p UnificationError
e = (MGU, [(Path, UnificationError)]) -> Result MGU
forall a.
(a, [(Path, UnificationError)])
-> WriterT [(Path, UnificationError)] Identity a
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer (MGU
emptyMGU, [(Path
p,UnificationError
e)])


newtype Path = Path [PathElement]
  deriving (Int -> Path -> ShowS
[Path] -> ShowS
Path -> String
(Int -> Path -> ShowS)
-> (Path -> String) -> ([Path] -> ShowS) -> Show Path
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Path -> ShowS
showsPrec :: Int -> Path -> ShowS
$cshow :: Path -> String
show :: Path -> String
$cshowList :: [Path] -> ShowS
showList :: [Path] -> ShowS
Show,(forall x. Path -> Rep Path x)
-> (forall x. Rep Path x -> Path) -> Generic Path
forall x. Rep Path x -> Path
forall x. Path -> Rep Path x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Path -> Rep Path x
from :: forall x. Path -> Rep Path x
$cto :: forall x. Rep Path x -> Path
to :: forall x. Rep Path x -> Path
Generic,Path -> ()
(Path -> ()) -> NFData Path
forall a. (a -> ()) -> NFData a
$crnf :: Path -> ()
rnf :: Path -> ()
NFData)

data PathElement =
    TConArg     TC      Int
  | TNominalArg NominalType Int
  | TRecArg     Ident
  deriving (Int -> PathElement -> ShowS
[PathElement] -> ShowS
PathElement -> String
(Int -> PathElement -> ShowS)
-> (PathElement -> String)
-> ([PathElement] -> ShowS)
-> Show PathElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PathElement -> ShowS
showsPrec :: Int -> PathElement -> ShowS
$cshow :: PathElement -> String
show :: PathElement -> String
$cshowList :: [PathElement] -> ShowS
showList :: [PathElement] -> ShowS
Show,(forall x. PathElement -> Rep PathElement x)
-> (forall x. Rep PathElement x -> PathElement)
-> Generic PathElement
forall x. Rep PathElement x -> PathElement
forall x. PathElement -> Rep PathElement x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PathElement -> Rep PathElement x
from :: forall x. PathElement -> Rep PathElement x
$cto :: forall x. Rep PathElement x -> PathElement
to :: forall x. Rep PathElement x -> PathElement
Generic,PathElement -> ()
(PathElement -> ()) -> NFData PathElement
forall a. (a -> ()) -> NFData a
$crnf :: PathElement -> ()
rnf :: PathElement -> ()
NFData)

rootPath :: Path
rootPath :: Path
rootPath = [PathElement] -> Path
Path []

isRootPath :: Path -> Bool
isRootPath :: Path -> Bool
isRootPath (Path [PathElement]
xs) = [PathElement] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PathElement]
xs

extPath :: Path -> PathElement -> Path
extPath :: Path -> PathElement -> Path
extPath (Path [PathElement]
xs) PathElement
x = [PathElement] -> Path
Path (PathElement
x PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
: [PathElement]
xs)


emptyMGU :: MGU
emptyMGU :: MGU
emptyMGU = (Subst
emptySubst, [])

doMGU :: Type -> Type -> Result MGU
doMGU :: Type -> Type -> Result MGU
doMGU Type
t1 Type
t2 = Path -> Type -> Type -> Result MGU
mgu Path
rootPath Type
t1 Type
t2

mgu :: Path -> Type -> Type -> Result MGU

mgu :: Path -> Type -> Type -> Result MGU
mgu Path
_ (TUser Name
c1 [Type]
ts1 Type
_) (TUser Name
c2 [Type]
ts2 Type
_)
  | Name
c1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
c2 Bool -> Bool -> Bool
&& [Type]
ts1 [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
ts2  = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

mgu Path
p (TVar TVar
x) Type
t     = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
x Type
t
mgu Path
p Type
t (TVar TVar
x)     = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
x Type
t

mgu Path
p (TUser Name
_ [Type]
_ Type
t1) Type
t2 = Path -> Type -> Type -> Result MGU
mgu Path
p Type
t1 Type
t2
mgu Path
p Type
t1 (TUser Name
_ [Type]
_ Type
t2) = Path -> Type -> Type -> Result MGU
mgu Path
p Type
t1 Type
t2

mgu Path
p (TCon (TC TC
tc1) [Type]
ts1) (TCon (TC TC
tc2) [Type]
ts2)
  | TC
tc1 TC -> TC -> Bool
forall a. Eq a => a -> a -> Bool
== TC
tc2 =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (TC -> Int -> PathElement
TConArg TC
tc1 Int
i) | Int
i <- [ Int
0 .. ] ]
    in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths [Type]
ts1 [Type]
ts2

mgu Path
_ (TCon (TF TFun
f1) [Type]
ts1) (TCon (TF TFun
f2) [Type]
ts2)
  | TFun
f1 TFun -> TFun -> Bool
forall a. Eq a => a -> a -> Bool
== TFun
f2 Bool -> Bool -> Bool
&& [Type]
ts1 [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
ts2  = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

-- XXX: here we loose the information about where the constarint came from
mgu Path
_ Type
t1 Type
t2
  | TCon (TF TFun
_) [Type]
_ <- Type
t1, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Type
t1 Type -> Type -> Type
=#= Type
t2])
  | TCon (TF TFun
_) [Type]
_ <- Type
t2, Bool
isNum, Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2 = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [Type
t1 Type -> Type -> Type
=#= Type
t2])
  where
  k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
  k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2

  isNum :: Bool
isNum = Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum

mgu Path
p (TRec RecordMap Ident Type
fs1) (TRec RecordMap Ident Type
fs2)
  | RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs1 Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs2 =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (Ident -> PathElement
TRecArg Ident
i) | (Ident
i,Type
_) <- RecordMap Ident Type -> [(Ident, Type)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident Type
fs1 ]
    in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs1) (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs2)

mgu Path
p (TNominal NominalType
ntx [Type]
xs) (TNominal NominalType
nty [Type]
ys)
  | NominalType
ntx NominalType -> NominalType -> Bool
forall a. Eq a => a -> a -> Bool
== NominalType
nty =
    let paths :: [Path]
paths = [ Path -> PathElement -> Path
extPath Path
p (NominalType -> Int -> PathElement
TNominalArg NominalType
ntx Int
i) | Int
i <- [ Int
0 .. ] ]
    in Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
paths [Type]
xs [Type]
ys

mgu Path
p Type
t1 Type
t2
  | Bool -> Bool
not (Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k2)  = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
  | Bool
otherwise       = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnificationError
UniTypeMismatch Type
t1 Type
t2
  where
  k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
  k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2


-- XXX: could pass the path to the lists themselvs
mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
_ [Path]
_ [] [] = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU
mguMany Path
p (Path
p1:[Path]
ps) (Type
t1 : [Type]
ts1) (Type
t2 : [Type]
ts2) =
  do (Subst
su1,[Type]
ps1) <- Path -> Type -> Type -> Result MGU
mgu Path
p1 Type
t1 Type
t2
     (Subst
su2,[Type]
ps2) <- Path -> [Path] -> [Type] -> [Type] -> Result MGU
mguMany Path
p [Path]
ps (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
ts1) (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
ts2)
     MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Type]
ps1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ps2)
mguMany Path
p [Path]
_ [Type]
t1 [Type]
t2 = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Int -> Int -> UnificationError
UniTypeLenMismatch ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
t1) ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
t2)
-- XXX: I think by this point the types should have been kind checked,
-- so there should be no mismatches with the lengths...


bindVar :: Path -> TVar -> Type -> Result MGU

bindVar :: Path -> TVar -> Type -> Result MGU
bindVar Path
_ TVar
x (Type -> Type
tNoUser -> TVar TVar
y)
  | TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y                      = MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MGU
emptyMGU

bindVar Path
p v :: TVar
v@(TVBound {})
          (Type -> Type
tNoUser -> TVar v1 :: TVar
v1@(TVFree {})) = Path -> TVar -> Type -> Result MGU
bindVar Path
p TVar
v1 (TVar -> Type
TVar TVar
v)

bindVar Path
p v :: TVar
v@(TVBound {}) Type
t
  | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t = if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum
                       then MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Type
TVar TVar
v Type -> Type -> Type
=#= Type
t])
                       else Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> UnificationError
UniNonPoly TVar
v Type
t
  | Bool
otherwise     = Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k (Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t)
  where k :: Kind
k = TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
v

bindVar Path
_ x :: TVar
x@(TVFree Int
_ Kind
xk Set TParam
xscope TVarInfo
_) (Type -> Type
tNoUser -> TVar y :: TVar
y@(TVFree Int
_ Kind
yk Set TParam
yscope TVarInfo
_))
  | Set TParam
xscope Set TParam -> Set TParam -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isProperSubsetOf` Set TParam
yscope, Kind
xk Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
yk =
    MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar -> Type -> Subst
uncheckedSingleSubst TVar
y (TVar -> Type
TVar TVar
x), [])
    -- In this case, we can add the reverse binding y ~> x to the
    -- substitution, but the instantiation x ~> y would be forbidden
    -- because it would allow y to escape from its scope.

bindVar Path
p TVar
x Type
t =
  case TVar -> Type -> Either SubstError Subst
singleSubst TVar
x Type
t of
    Left SubstError
SubstRecursive
      | TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KType -> Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> Type -> UnificationError
UniRecursive TVar
x Type
t
      | Bool
otherwise -> MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
emptySubst, [TVar -> Type
TVar TVar
x Type -> Type -> Type
=#= Type
t])
    Left (SubstEscaped [TParam]
tps) ->
      Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ TVar -> [TParam] -> UnificationError
UniNonPolyDepends TVar
x [TParam]
tps
    Left (SubstKindMismatch Kind
k1 Kind
k2) ->
      Path -> UnificationError -> Result MGU
uniError Path
p (UnificationError -> Result MGU) -> UnificationError -> Result MGU
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> UnificationError
UniKindMismatch Kind
k1 Kind
k2
    Right Subst
su ->
      MGU -> Result MGU
forall a. a -> WriterT [(Path, UnificationError)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su, [])


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

ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
el Int
prec Int -> Doc
k =
  case PathElement
el of
    TRecArg Ident
l -> Doc -> Doc
braces (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
0 Doc -> Doc -> Doc
<.> Doc
comma Doc -> Doc -> Doc
<+> Doc
"…")

    TConArg TC
tc Int
n ->
      case TC
tc of

       TC
TCSeq -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4)
                if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Doc -> Doc
brackets (Int -> Doc
k Int
0) Doc -> Doc -> Doc
<+> Doc
"_"
                          else Doc -> Doc
brackets Doc
"_" Doc -> Doc -> Doc
<+> (Int -> Doc
k Int
4)

       TC
TCFun -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)
                if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Int -> Doc
k Int
2 Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Doc
"_"
                          else Doc
"_" Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Int -> Doc
k Int
1

       TCTuple Int
i  -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
0] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
          where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
                after :: [Doc]
after  = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"

       TC
_ -> Int -> Doc -> Int -> Doc
justPrefix (Kind -> Int
forall {a}. Num a => Kind -> a
kindArity (TC -> Kind
forall t. HasKind t => t -> Kind
kindOf TC
tc)) (TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc) Int
n

    TNominalArg NominalType
nt Int
n ->
      Int -> Doc -> Int -> Doc
justPrefix ([TParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NominalType -> [TParam]
ntParams NominalType
nt)) (Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent (NominalType -> Name
ntName NominalType
nt))) Int
n

  where
  justPrefix :: Int -> Doc -> Int -> Doc
justPrefix Int
arity Doc
fun Int
n =
    Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (Doc
fun Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ([Doc]
before [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc
k Int
5] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
after))
    where before :: [Doc]
before = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n Doc
"_"
          after :: [Doc]
after  = Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc
"_"

  kindArity :: Kind -> a
kindArity Kind
ki =
    case Kind
ki of
      Kind
_ :-> Kind
k1 -> a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Kind -> a
kindArity Kind
k1
      Kind
_        -> a
0

instance PP Path where
  ppPrec :: Int -> Path -> Doc
ppPrec Int
prec0 (Path [PathElement]
ps0) = [PathElement] -> Int -> Doc
go ([PathElement] -> [PathElement]
forall a. [a] -> [a]
reverse [PathElement]
ps0) Int
prec0
    where
    go :: [PathElement] -> Int -> Doc
go [PathElement]
ps Int
prec =
      case [PathElement]
ps of
        []       -> Doc
"ERROR"
        PathElement
p : [PathElement]
more -> PathElement -> Int -> (Int -> Doc) -> Doc
ppPathEl PathElement
p Int
prec ([PathElement] -> Int -> Doc
go [PathElement]
more)