patterns not matched

patterns-not-matched.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

module GADTS where

-- Some universe of types
data Universe = A
              | B

-- Singleton support
data SUniverse (u :: Universe) :: * where
    SA :: SUniverse A
    SB :: SUniverse B

-- Some interfaces we pass our universe types through
data Interface = UDP
               | TCP

-- singleton support
data SInterface (i :: Interface) :: * where
    SUDP :: SInterface UDP
    STCP :: SInterface TCP

-- Type family to represent input data
type family InputData (u :: Universe) (i :: Interface) :: * where
    InputData A UDP = Int
    InputData A TCP = String
    InputData B UDP = (String, String)
    -- InputData purposefully not defined for B x TCP.

-- Some functor
data MyFunctor :: * where
    MyFunctor :: SUniverse u
              -> SInterface i
              -> InputData u i
              -> MyFunctor

-- an interpreter to show pattern matching non-exhaustive error
interpreter :: MyFunctor -> IO ()
interpreter (MyFunctor SA SUDP i) = print i
interpreter (MyFunctor SA STCP s) = putStrLn s
interpreter (MyFunctor SB SUDP (a,_)) = print a

{-

compiling this yields error:

gadts.hs|41 col 1 warning| Pattern match(es) are non-exhaustive
|| In an equation for ‘interpreter’:
||     Patterns not matched: MyFunctor SB STCP _ _

even though we have not defined `InputData B TCP` and therefore trying
to construct a value like `x = MyFunctor SB STCP ...` should give an error (see below)

-}

-- | for the below examples, the pattern matches warning still displays
-- but I though they might be useful details for this issue.

-- Note: this will compile as it should.
willCompile :: MyFunctor
willCompile = MyFunctor SB SUDP ("foo","bar")

{- Note: this will not compile, as it shouldn't because we have not defined `InputData SB SUDP`

willNotCompile :: MyFunctor
willNotCompile = MyFunctor SB STCP (1,2)

The error:

gadts.hs|63 col 36 error| Couldn't match expected type ‘GADTS.InputData 'GADTS.B 'GADTS.TCP’
||             with actual type ‘(t0, t1)’
|| The type variables ‘t0’, ‘t1’ are ambiguous 
|| In the third argument of ‘GADTS.MyFunctor’, namely ‘(1, 2)’
|| In the expression: GADTS.MyFunctor GADTS.SB GADTS.STCP (1, 2)
|| In an equation for ‘willNotCompile’:
||     willNotCompile = GADTS.MyFunctor GADTS.SB GADTS.STCP (1, 2)

-}

-- However, this does compile, and it probably shouldn't
doesCompileButShouldnt :: MyFunctor
doesCompileButShouldnt = MyFunctor SB STCP undefined