Is there a way to get a compile-time error if there's no matching closed type family instance?

Question

I have a closed type family which has no catch-all case:

{-# LANGUAGE TypeFamilies #-}

type family Foo a where
    Foo Bool = Int
    Foo Int = Bool

Is there a way to force the type checker to reject the following program:

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

on account of the fact that there is no Foo String type?

Answer 1

Starting from GHC 8.0.1, it's possible to write:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

import GHC.TypeLits

type family Foo a where
    Foo Bool = Int
    Foo Int  = Bool
    Foo a    = TypeError (Text "Invalid Foo " :<>: ShowType a)

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

Module can be loaded, yet you cannot use x:

*Main> :r
[1 of 1] Compiling Main             ( te.hs, interpreted )
Ok, modules loaded: Main.
*Main> x

<interactive>:18:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        it :: T (TypeError ...)

If you add, without a type signature

y = id x

the GHC(i) while complain during type-check:

te.hs:15:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        y :: T (TypeError ...)

Yet, if you give y a type: y :: T (Foo String); then GHC will accept that as well.

I'm not sure whether this is a bug or feature. Type families, even closed one, cannot be arbitrarily reduced, especially in presence of UndecidableInstances, which one needs to use TypeError in the first place. And even something like whnf is probably not enough, if type family would reduce to Maybe (TypeError ...).