{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- Module      :  Disco.Typecheck.Constraints
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Constraints generated by type inference & checking.
module Disco.Typecheck.Constraints (
  Constraint (..),
  cAnd,
  cOr,
)
where

import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Semigroup
import Disco.Effects.LFresh
import Disco.Pretty hiding ((<>))
import Disco.Syntax.Operators (BFixity (In, InL, InR))
import Disco.Types
import Disco.Types.Rules
import GHC.Generics (Generic)
import Unbound.Generics.LocallyNameless hiding (lunbind)

-- | Constraints are generated as a result of type inference and checking.
--   These constraints are accumulated during the inference and checking phase
--   and are subsequently solved by the constraint solver.
data Constraint where
  CSub :: Type -> Type -> Constraint
  CEq :: Type -> Type -> Constraint
  CQual :: Qualifier -> Type -> Constraint
  CAnd :: NonEmpty Constraint -> Constraint
  CTrue :: Constraint
  COr :: NonEmpty Constraint -> Constraint
  CAll :: Bind [Name Type] Constraint -> Constraint
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show, (forall x. Constraint -> Rep Constraint x)
-> (forall x. Rep Constraint x -> Constraint) -> Generic Constraint
forall x. Rep Constraint x -> Constraint
forall x. Constraint -> Rep Constraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Constraint -> Rep Constraint x
from :: forall x. Constraint -> Rep Constraint x
$cto :: forall x. Rep Constraint x -> Constraint
to :: forall x. Rep Constraint x -> Constraint
Generic, Show Constraint
Show Constraint =>
(AlphaCtx -> Constraint -> Constraint -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint)
-> (AlphaCtx -> NamePatFind -> Constraint -> Constraint)
-> (AlphaCtx -> NthPatFind -> Constraint -> Constraint)
-> (Constraint -> DisjointSet AnyName)
-> (Constraint -> All)
-> (Constraint -> Bool)
-> (Constraint -> NthPatFind)
-> (Constraint -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Constraint -> Constraint)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Constraint -> m (Constraint, Perm AnyName))
-> (AlphaCtx -> Constraint -> Constraint -> Ordering)
-> Alpha Constraint
AlphaCtx -> Perm AnyName -> Constraint -> Constraint
AlphaCtx -> NamePatFind -> Constraint -> Constraint
AlphaCtx -> NthPatFind -> Constraint -> Constraint
AlphaCtx -> Constraint -> Constraint -> Bool
AlphaCtx -> Constraint -> Constraint -> Ordering
Constraint -> Bool
Constraint -> All
Constraint -> NamePatFind
Constraint -> NthPatFind
Constraint -> DisjointSet AnyName
forall a.
Show a =>
(AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
$caeq' :: AlphaCtx -> Constraint -> Constraint -> Bool
aeq' :: AlphaCtx -> Constraint -> Constraint -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint
$cclose :: AlphaCtx -> NamePatFind -> Constraint -> Constraint
close :: AlphaCtx -> NamePatFind -> Constraint -> Constraint
$copen :: AlphaCtx -> NthPatFind -> Constraint -> Constraint
open :: AlphaCtx -> NthPatFind -> Constraint -> Constraint
$cisPat :: Constraint -> DisjointSet AnyName
isPat :: Constraint -> DisjointSet AnyName
$cisTerm :: Constraint -> All
isTerm :: Constraint -> All
$cisEmbed :: Constraint -> Bool
isEmbed :: Constraint -> Bool
$cnthPatFind :: Constraint -> NthPatFind
nthPatFind :: Constraint -> NthPatFind
$cnamePatFind :: Constraint -> NamePatFind
namePatFind :: Constraint -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Constraint -> Constraint
swaps' :: AlphaCtx -> Perm AnyName -> Constraint -> Constraint
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
$cacompare' :: AlphaCtx -> Constraint -> Constraint -> Ordering
acompare' :: AlphaCtx -> Constraint -> Constraint -> Ordering
Alpha, Subst Type)

instance Pretty Constraint where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Constraint -> Sem r (Doc ann)
pretty = \case
    CSub Type
ty1 Type
ty2 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"<:" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
    CEq Type
ty1 Type
ty2 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
    CQual Qualifier
q Type
ty -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
10 BFixity
InL) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Qualifier -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Qualifier -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Qualifier
q) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty)
    -- Use rt for everything, since we don't need to print parens for /\ at all
    CAnd NonEmpty Constraint
cs -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
3 BFixity
InR) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann))
-> NonEmpty (Sem r (Doc ann)) -> Sem r (Doc ann)
forall a. (a -> a -> a) -> NonEmpty a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Sem r (Doc ann)
a Sem r (Doc ann)
b -> Sem r (Doc ann)
a Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"/\\" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
b) ((Constraint -> Sem r (Doc ann))
-> NonEmpty Constraint -> NonEmpty (Sem r (Doc ann))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Sem r (Doc ann) -> Sem r (Doc ann))
-> (Constraint -> Sem r (Doc ann)) -> Constraint -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Constraint -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty) NonEmpty Constraint
cs)
    Constraint
CTrue -> Sem r (Doc ann)
"True"
    COr NonEmpty Constraint
cs -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
2 BFixity
InR) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann))
-> NonEmpty (Sem r (Doc ann)) -> Sem r (Doc ann)
forall a. (a -> a -> a) -> NonEmpty a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Sem r (Doc ann)
a Sem r (Doc ann)
b -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt Sem r (Doc ann)
a Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"\\/" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt Sem r (Doc ann)
b) ((Constraint -> Sem r (Doc ann))
-> NonEmpty Constraint -> NonEmpty (Sem r (Doc ann))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map Constraint -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Constraint -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty NonEmpty Constraint
cs)
    CAll Bind [Name Type] Constraint
b -> Bind [Name Type] Constraint
-> (([Name Type], Constraint) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Constraint
b ((([Name Type], Constraint) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([Name Type], Constraint) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([Name Type]
xs, Constraint
c) ->
      Sem r (Doc ann)
"∀" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ((Name Type -> Sem r (Doc ann)) -> [Name Type] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Name Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Type]
xs) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"." Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Constraint -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Constraint -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c

-- A helper function for creating a single constraint from a list of constraints.
cAnd :: [Constraint] -> Constraint
cAnd :: [Constraint] -> Constraint
cAnd [Constraint]
cs = case (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter Constraint -> Bool
nontrivial [Constraint]
cs of
  [] -> Constraint
CTrue
  [Constraint
c] -> Constraint
c
  (Constraint
c : [Constraint]
cs') -> NonEmpty Constraint -> Constraint
CAnd (Constraint
c Constraint -> [Constraint] -> NonEmpty Constraint
forall a. a -> [a] -> NonEmpty a
:| [Constraint]
cs')
 where
  nontrivial :: Constraint -> Bool
nontrivial Constraint
CTrue = Bool
False
  nontrivial Constraint
_ = Bool
True

cOr :: [Constraint] -> Constraint
cOr :: [Constraint] -> Constraint
cOr [] = String -> Constraint
forall a. HasCallStack => String -> a
error String
"Empty list of constraints in cOr"
cOr [Constraint
c] = Constraint
c
cOr (Constraint
c : [Constraint]
cs) = NonEmpty Constraint -> Constraint
COr (Constraint
c Constraint -> [Constraint] -> NonEmpty Constraint
forall a. a -> [a] -> NonEmpty a
:| [Constraint]
cs)

instance Semigroup Constraint where
  Constraint
c1 <> :: Constraint -> Constraint -> Constraint
<> Constraint
c2 = [Constraint] -> Constraint
cAnd [Constraint
c1, Constraint
c2]
  sconcat :: NonEmpty Constraint -> Constraint
sconcat = [Constraint] -> Constraint
cAnd ([Constraint] -> Constraint)
-> (NonEmpty Constraint -> [Constraint])
-> NonEmpty Constraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Constraint -> [Constraint]
forall a. NonEmpty a -> [a]
NE.toList
  stimes :: forall b. Integral b => b -> Constraint -> Constraint
stimes = b -> Constraint -> Constraint
forall b a. Integral b => b -> a -> a
stimesIdempotent

instance Monoid Constraint where
  mempty :: Constraint
mempty = Constraint
CTrue
  mappend :: Constraint -> Constraint -> Constraint
mappend = Constraint -> Constraint -> Constraint
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [Constraint] -> Constraint
mconcat = [Constraint] -> Constraint
cAnd