Type Families which are clearly total

[ahubers]

See this commit:

https://github.com/IaFP/ghc/pull/24/commits/291d8f37817d892973743ed8903792349a1f261c

We have the following (DataKind'ed) code:

data GhcPass (c :: Pass) where
  GhcPs :: GhcPass 'Parsed
  GhcRn :: GhcPass 'Renamed
  GhcTc :: GhcPass 'Typechecked

type GhcPs   = GhcPass 'Parsed
type GhcRn   = GhcPass 'Renamed
type GhcTc   = GhcPass 'Typechecked

type family NoGhcTcPass (p :: Pass) :: Pass where
  NoGhcTcPass 'Typechecked = 'Renamed
  NoGhcTcPass other        = other

Now, both you and I know that if an application (NoGhcTcPass p) is well-kinded, then it's total. But I don't know how to express that within our framework of partiality constraints. Further, we know that if (NoGhcTcPass p) is total from Pass -> Pass, then (NoGhcTcPass (NoGhcTcPass p)) is defined! Nevertheless, I need to add

WFT (NoGhcTcPass (NoGhcTcPass p))

constraints to functions. Which seems silly.

[ahubers]

I don't really know what to do with this -- and it's neither high priority nor really needs resolution, but I'm logging just in case anyone else has thoughts.

[fxdpntthm]

something something infinite type family reduction something something..

[jgbm]

Hmm.

Here is some valid Haskell code:

type family F a where
    F Int = Bool
    F _   = Bool

foo :: F a -> Bool
foo = not

type family WF_F a :: Constraint where
    WF_F Int = ()
    WF_F _   = ()

g :: WF_F a => F a -> Bool
g = not

f :: F a -> Bool
f = g

foo can have to F a -> a because closed type families have a rule that basically allows you to rewrite with multiple matching equations so long as they all have the same RHS.

f can be defined to be g for the same reason: it rewrite WF_F a without knowing a because both equations have the same RHS.

It seems like this should applying to the instance generated by NoGhcTcPass as well. What instance are we actually generating there?

[ahubers]

So, your example generates:

TYPE SIGNATURES
  foo :: forall a. $wf'F a => F a -> Bool
TYPE CONSTRUCTORS
  type family $wf'F{1} :: * -> Constraint
    roles nominal
  type family F{1} :: * -> *
    roles nominal
COERCION AXIOMS
  axiom Hmm.D:R:F ::
      F Int = Bool
      F _1 = Bool
  axiom Hmm.D:R:$wf'F ::
      $wf'F Int = () :: Constraint
      $wf'F _1 = () :: Constraint

And the NoGhcTcPass example generates:

TYPE CONSTRUCTORS
  type family $wf'NoGhcTcPass{1} :: Pass -> Constraint
    roles nominal
  data type GhcPass{1} :: Pass -> *
    roles nominal
  type synonym GhcPs{0} :: *
  type synonym GhcRn{0} :: *
  type synonym GhcTc{0} :: *
  type family NoGhcTcPass{1} :: Pass -> Pass
    roles nominal
  data type Pass{0} :: *
COERCION AXIOMS
  axiom Hmm.D:R:NoGhcTcPass ::
      NoGhcTcPass 'Typechecked = 'Renamed
      NoGhcTcPass other = other
  axiom Hmm.D:R:$wf'NoGhcTcPass ::
      $wf'NoGhcTcPass 'Typechecked = () :: Constraint
      $wf'NoGhcTcPass other = () :: Constraint
DATA CONSTRUCTORS
  GhcPs :: GhcPass 'Parsed
  GhcRn :: GhcPass 'Renamed
  GhcTc :: GhcPass 'Typechecked
  Parsed :: Pass
  Renamed :: Pass
  Typechecked :: Pass
FAMILY INSTANCES
  type instance GhcPass @ c = () :: Constraint
                  -- Defined at testsuite/tests/party-ctrs/type-families/DebugCases/Hmm.hs:10:1

[ahubers]

You are right, foo does not complain about being defined as not because GHC seems able to tell that F a always reduces to Bool -- but oddly, we still affix $wf'F a to foo's signature, even though I try to only do that in the case that F a does not reduce.

[jgbm]

Not quite the point I wanted to make. My example attempts to simulate at WF constraint for F, and that GHC can discharge it automatically (otherwise f = g wouldn't type).

The way I see it, the same thing should happen for $wf'NoGhcTcPass---because the RHS is the same, GHC should be able to discharge $wf'NoGhcTcPass T for any old T you come across. We should never need to add it to a constraint.

[fxdpntthm]

both you and I know that if an application (NoGhcTcPass p) is well-kinded, then it's total.

We know this only after we look at the definition. We cannot however know this if NoGhcTcPass is declared in a boot file but defined in its main file. This is related to #26

[ahubers]

Just an update that I was able to remove the WFT (NoGhcTcPass p) and WFT (NoGhcTcPass (NoGhcTcPass p)) constraints for the reason you mentioned @jgbm (after adding some logic to reduce closed TF applications in constraints). https://github.com/IaFP/ghc/commit/e06fef215a4aa46a13d9791c5a99f7ef7311b026