GHC does not warn about redundant patterns

Given the D1535 effort in GHC 8.0 I was curious how an example from Richard's post What are type families? would fare:

% ghci -Wall -XTypeFamilies -ignore-dot-ghci
GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help
Prelude> :set +m
Prelude> type family F1 a where
Prelude| F1 Int = Bool
Prelude|
Prelude> let
Prelude| sillyId :: F1 Char -> F1 Char
Prelude| sillyId x = x
Prelude|
Prelude>

This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using EmptyCase (#2431 (closed)) as sillyId = \case? It seems GHC doesn't care that the pattern match in the equation absurd2 _ = ... is redundant either:

data Void
absurd1 :: Void -> a
absurd1 = \case
absurd2 :: Void -> a
absurd2 _ = undefined

Is this intended or known behaviour?