GADTs in record not propagating constraint

[claudeha]

{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE NoFieldSelectors #-}

type Time = Rational

newtype Note = Note Double
  deriving (Eq, Ord, Read, Show, Enum, Num, Fractional, Real, RealFrac, Floating, RealFloat)

data Pattern a = Pattern {query :: () -> [Maybe a]}
  deriving (Functor)

data Pat a where
    PNote :: Pat Note
    PDouble :: Pat Double
    PStr :: Pat String
    PInt :: Pat Int
    PTime :: Pat Time
    PBool :: Pat Bool

data MondoPat a b = MondoPat
    { pat :: Pat a
    , patToControl :: Pattern a -> Pattern b
    }

fromInt :: MondoPat a b -> Maybe (Pattern Int -> Pattern b)
fromInt mpat = case mpat.pat of
    PNote -> Just (mpat.patToControl . fmap fromIntegral)
    PInt -> Just mpat.patToControl
    _ -> Nothing

ghci 9.12 accepts
mhs 0.15.5 says cannot satisfy Num a

(this example is derived from the tidal-mondo package)

[claudeha]

type MondoPat a b = (Pat a, Pattern a -> Pattern b)

fromInt :: MondoPat a b -> Maybe (Pattern Int -> Pattern b)
fromInt mpat = case mpat of
    (PNote, to) -> Just (to . fmap fromIntegral)
    (PInt, to) -> Just to
    _ -> Nothing

this version is accepted by both ghci and mhs

[augustss]

If you use pat mpat instead of mpat.pat it also works.

There is something wrong with the equality constraint solving. Since that will change with type families I will leave this bug open until I'm done with type families.