Is it possible to infer a type that is a reflection-like closure?

Question

With the following "toy model" of Clash:

{-# LANGUAGE RankNTypes, KindSignatures, DataKinds, FlexibleContexts #-}

-- Simplified model of platform definitions
data Domain = DomSys | Dom25

data Signal (dom :: Domain)
data Clock (dom :: Domain)

class HiddenClock (dom :: Domain)

withClock :: Clock dom -> (HiddenClock dom => r) -> r
withClock _ _ = undefined

I would like to use withClock to close over the HiddenClock constraint inside a local where block. Suppose I have the following two toplevel definitions:

-- Simplified model of external standalone definitions
mainBoard :: (HiddenClock dom) => Signal dom -> Signal dom -> Signal dom -> (Signal dom, Signal dom)
mainBoard = undefined

peripherals :: (HiddenClock dom) => Signal dom -> Signal dom
peripherals = undefined

video
    :: Clock domVid
    -> Clock domSys
    -> Signal domSys
    -> Signal domSys
    -> (Signal domVid, Signal domSys, Signal domSys)
video = undefined

then, I would like to write something like the following:

topEntity :: Clock Dom25 -> Clock DomSys -> Signal DomSys -> Signal Dom25
topEntity clkVid clkSys input = vga
  where
    (vga, vidRead, line) = video clkVid clkSys vidAddr vidWrite
    (vidAddr, vidWrite) = withClock clkSys board

    board = mainBoard vidRead line p
      where
        p = peripherals input

Unfortunately, GHC (at least as of 8.10.7) is unable to infer the correct type for board, which causes withClock clkSys board to not really close over the HiddenClock DomSys constriant:

    • No instance for (HiddenClock 'DomSys)
        arising from a use of ‘mainBoard’
    • In the expression: mainBoard vidRead line p
      In an equation for ‘board’:
          board
            = mainBoard vidRead line p
            where
                p = peripherals input
      In an equation for ‘topEntity’:
          topEntity clkVid clkSys input
            = vga
            where
                (vga, vidRead, line) = video clkVid clkSys vidAddr vidWrite
                (vidAddr, vidWrite) = withClock clkSys board
                board
                  = mainBoard vidRead line p
                  where
                      p = peripherals input
   |
38 |     board = mainBoard vidRead line p
   |             ^^^^^^^^^^^^^^^^^^^^^^^^

    • No instance for (HiddenClock 'DomSys)
        arising from a use of ‘peripherals’
    • In the expression: peripherals input
      In an equation for ‘p’: p = peripherals input
      In an equation for ‘board’:
          board
            = mainBoard vidRead line p
            where
                p = peripherals input
   |
40 |         p = peripherals input
   |             ^^^^^^^^^^^^^^^^^

This can be worked around by adding a type signature to board:

    board :: (HiddenClock DomSys) => (Signal DomSys, Signal DomSys)

My question is: is it possible to change this code slightly, or fiddle with the exact type of withClock etc., to make this definition of topEntity typecheck without a type signature on the binding of board?

Answer 1

I don't think you can really infer this and I'm not entirely sure why you need to. In Clash HiddenClock uses ImplicitParams under the hood. Currently, your board has no way of knowing where the clock is coming from.

You need to either pass the clock by value clkSys or explicitly write that the clock is needed at the type level with a HiddenClock constraint.

ImplicitParams don't really work like normal type class constraints. This HiddenClock isn't a constraint on the dom. And you can see that by the fact that HiddenClock 'DomSys is still needed as a constraint, even though it has no free variables.

Here is an example using plain Haskell (with ImplicitParams) of your issue:

{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}

module Temp where

withX :: Int -> ((?x :: Int) => r) -> r
withX x r =
  let ?x = x
  in r

somethingThanNeedsX :: (?x :: Int) => Int
somethingThanNeedsX = ?x + 2

foo :: Int
foo = bar
  where
    bar = withX 42 baz

    baz = somethingThanNeedsX

And GHC tells me:

Orig.hs:19:11: error:
    • Unbound implicit parameter (?x::Int)
        arising from a use of ‘somethingThanNeedsX’
    • In the expression: somethingThanNeedsX
      In an equation for ‘baz’: baz = somethingThanNeedsX
      In an equation for ‘foo’:
          foo
            = bar
            where
                bar = withX 42 baz
                baz = somethingThanNeedsX
   |
19 |     baz = somethingThanNeedsX
   |      

In order to make this work, you either need to have withX in the definition of baz (explicitly passing x/the clock there) or be explicit about the ImplicitParams dependency. You don't need a full type signature if you don't want to, you just need the ImplicitParams constraint (using PartialTypeSignatures):

{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}

module Temp where

withX :: Int -> ((?x :: Int) => r) -> r
withX x r =
  let ?x = x
  in r

somethingThanNeedsX :: (?x :: Int) => Int
somethingThanNeedsX = ?x + 2

foo :: Int
foo = bar
  where
    bar = withX 42 baz

    baz :: (?x :: Int) => _
    baz = somethingThanNeedsX

This now compiles just fine (with a warning that can be disabled with {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} if you really want):

Temp.hs:20:27: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘Int’
    • In the type signature: baz :: (?x :: Int) => _
      In an equation for ‘foo’:
          foo
            = bar
            where
                bar = withX 42 baz
                baz :: (?x :: Int) => _
                baz = somethingThanNeedsX
    • Relevant bindings include foo :: Int (bound at Temp.hs:16:1)
   |
20 |     baz :: (?x :: Int) => _
   |